[nogin] Fixed some _this expression should have type unit_ Ocaml_2.01 warnings_ Mon Sep 19 02:07:39 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-07-39-238679000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-07-39-238679000-PDT.html [lolorigo] added improvements to mathbus speed, and functionality for edits in nuprl_ Mon Sep 19 02:07:41 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-07-41-559243000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-07-41-559243000-PDT.html [nogin] Copied the DAG_based unification algorithm_ Mon Sep 19 02:07:42 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-07-42-499176000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-07-42-499176000-PDT.html [jyh] Numerous minor changes._ Mon Sep 19 02:07:44 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-07-44-213839000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-07-44-213839000-PDT.html [nogin] Cleenup_ Mon Sep 19 02:07:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-07-53-672281000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-07-53-672281000-PDT.html [jyh] Proof expansion works._ Mon Sep 19 02:07:55 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-07-55-351209000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-07-55-351209000-PDT.html [jyh] Added _kreitz_ command to fold up an entire proof subtree into a single node._ Mon Sep 19 02:07:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-07-56-388583000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-07-56-388583000-PDT.html [jyh] Added pigeonhole problem in editor/ml/test.ml._ Mon Sep 19 02:07:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-07-58-284510000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-07-58-284510000-PDT.html [jyh] Added pigeonhole generator._ Mon Sep 19 02:07:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-07-59-070457000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-07-59-070457000-PDT.html [jyh] The general intuitionistic propDecideT now works._ Mon Sep 19 02:08:00 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-00-820992000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-00-820992000-PDT.html [nogin] Made bound_term__bound_term._ Mon Sep 19 02:08:01 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-01-368893000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-01-368893000-PDT.html [nogin] Small efficiency fixes._ Mon Sep 19 02:08:02 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-02-399123000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-02-399123000-PDT.html [nogin] Pushed Sequent.hyp_indices down into the Term_man_ Mon Sep 19 02:08:02 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-02-798089000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-02-798089000-PDT.html [nogin] Fixed the bytecode profiling build._ Mon Sep 19 02:08:04 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-04-493215000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-04-493215000-PDT.html [nogin] Inlined extract_sequent_terms._ Mon Sep 19 02:08:04 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-04-896138000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-04-896138000-PDT.html [nogin] Do not call get_core unless the sequent is actually a delayed substitution._ Mon Sep 19 02:08:05 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-05-267011000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-05-267011000-PDT.html [jyh] Added module_checking function _expand_all_ to the Shell module._ Mon Sep 19 02:08:05 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-05-702026000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-05-702026000-PDT.html [nogin] The list of include directories is now defined in mpconfig_ Mon Sep 19 02:08:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-07-451775000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-07-451775000-PDT.html [nogin] debug_unify_ Mon Sep 19 02:08:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-07-870728000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-07-870728000-PDT.html [nogin] debug_alpha_equal_ Mon Sep 19 02:08:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-08-275328000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-08-275328000-PDT.html [jyh] Faster propDecideT._ Mon Sep 19 02:08:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-08-703949000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-08-703949000-PDT.html [nogin] Print terms in debug_alpha_equal_ Mon Sep 19 02:08:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-10-368585000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-10-368585000-PDT.html [nogin] Fixed debug_ Mon Sep 19 02:08:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-10-762880000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-12/2005-09-19-02-08-10-762880000-PDT.html