[nogin] Updated the list of people who contirbuted code to MetaPRL._ Mon Sep 19 02:38:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-38-36-999911000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-38-36-999911000-PDT.html [nogin] Fixed links._ Mon Sep 19 02:38:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-38-37-534834000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-38-37-534834000-PDT.html [cwitty] Started changing declare/prim_rw to define _as in TODO 2.01.2_._ Mon Sep 19 02:38:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-38-37-935439000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-38-37-935439000-PDT.html [jyh] This jumbo update is a documentation update. There are no_ Mon Sep 19 02:38:39 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-38-39-159099000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-38-39-159099000-PDT.html [jyh] Last commit failed partway through..._ Mon Sep 19 02:39:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-39-58-350957000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-39-58-350957000-PDT.html [nogin] MetaPRL now requires an extra patch to by applied to Camlp4 __ Mon Sep 19 02:46:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-15-316020000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-15-316020000-PDT.html [yegor] First compilable version_ Mon Sep 19 02:46:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-15-830830000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-15-830830000-PDT.html [yegor] itt_int_bool_new was split into itt_int_base _beq_int, lt_bool, lt, add, uni_minus, sub, int, ind, number__ Mon Sep 19 02:46:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-16-608847000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-16-608847000-PDT.html [jyh] Sorry, the problem with the last commit was just because of the_ Mon Sep 19 02:46:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-17-410297000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-17-410297000-PDT.html [nogin] 1_ _define_ currently can_t handle recursive difinitions._ Mon Sep 19 02:46:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-21-607196000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-21-607196000-PDT.html [nogin] Documentation Makefiles hacking__ Mon Sep 19 02:46:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-22-198929000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-22-198929000-PDT.html [jyh] Fall back to CM fonts in the all_theories.tex file._ Mon Sep 19 02:46:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-22-663375000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-22-663375000-PDT.html [nogin] _ Ocamldep now treats _derive_ in the same way as _include_ and _open__ Mon Sep 19 02:46:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-23-053043000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-23-053043000-PDT.html [kopylov] 1_ Added a new theory _itt_disect_ about dependent intersection._ Mon Sep 19 02:46:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-23-688390000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-23-688390000-PDT.html [nogin] _ Added _ and sqeq to parser. For now, they produce Perv__rewrite_ terms,_ Mon Sep 19 02:46:24 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-24-533528000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-24-533528000-PDT.html [nogin] Removed some duplicated code._ Mon Sep 19 02:46:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-25-252276000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-25-252276000-PDT.html [nogin] JProver updates__ Mon Sep 19 02:46:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-25-863845000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-25-863845000-PDT.html [kopylov] I split the Itt_set theory into Itt_hide and Itt_set._ Mon Sep 19 02:46:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-33-336326000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-33-336326000-PDT.html [nogin] Bob_s _Agatha_ puzzle._ Mon Sep 19 02:46:38 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-38-225976000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-38-225976000-PDT.html [nogin] Some of the functions were not wrapped in print_exn for some reason _ fixed._ Mon Sep 19 02:46:38 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-38-620226000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-38-620226000-PDT.html [jyh] Update Itt_logic/implies_df to a nested dform _so it displays recursive_ Mon Sep 19 02:46:39 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-39-042586000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-39-042586000-PDT.html [jyh] Added terminal resizing as Alexey suggested._ Mon Sep 19 02:46:40 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-40-619615000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-40-619615000-PDT.html [jyh] Oops, that last checkin had a bug_ I forgot about the correct_ Mon Sep 19 02:46:43 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-43-492695000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-43-492695000-PDT.html [nogin] The result of MP toploop expression evaluation is now also formatted_ Mon Sep 19 02:46:45 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-45-997375000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2000-09/2005-09-19-02-46-45-997375000-PDT.html