Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-01 08:10:05 -0800 (Fri, 01 Jan 1999)
Revision: 2545
Log message:

      This is supposed to fix alpha_equal.
      Can somebody double-check me? Thanks.
      

Changes  Path
+8 -0 metaprl/mllib/list_util.ml
+1 -0 metaprl/mllib/list_util.mli
+15 -5 metaprl/refiner/term_ds/term_subst_ds.mlp
+2 -15 metaprl/refiner/term_std/term_subst_std.mlp

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-01 09:46:03 -0800 (Fri, 01 Jan 1999)
Revision: 2546
Log message:

      Fixed opname specification error in Itt_fset.
      

Changes  Path
+1 -1 metaprl/editor/ml/y.ml
Deleted metaprl/lib/mbs-mpl.txt
+3 -1 metaprl/library/Makefile
Added metaprl/library/mbs-mpl.txt
Properties metaprl/library/mbs-mpl.txt
+1 -1 metaprl/theories/itt/itt_fset.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-01 09:51:22 -0800 (Fri, 01 Jan 1999)
Revision: 2547
Log message:

      This file produces different results with Term_ds and Term_std,
      even after alpha_equal is fixed.
      

Changes  Path
Added metaprl/editor/ml/bad.ml
Properties metaprl/editor/ml/bad.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-01 12:08:15 -0800 (Fri, 01 Jan 1999)
Revision: 2548
Log message:

      Fixed off-by-one error in nth_clause_addr.
      

Changes  Path
+5 -5 metaprl/refiner/term_gen/term_man_gen.mlp

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-01 12:14:13 -0800 (Fri, 01 Jan 1999)
Revision: 2549
Log message:

      Fixed up "make clean" to remove more files.
      The directory should be like a new checkout afterwards.
      Enabled set_debug function in toploop.  You can
      turn on debugging with
      
      # set_debug "xxx" true;;
      
      for some debug variable xxx.
      

Changes  Path
+1 -1 metaprl/editor/ml/Makefile
+2 -1 metaprl/editor/ml/shell.ml
+1 -0 metaprl/editor/ml/x.ml
+2 -0 metaprl/ensemble/Makefile
+2 -2 metaprl/mk/config
+2 -2 metaprl/theories/tactic/mptop.ml
+2 -1 metaprl/theories/tptp/Makefile

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-02 08:47:14 -0800 (Sat, 02 Jan 1999)
Revision: 2550
Log message:

      Fixed some problems with Ensemble.
      The closure marshaler was marshaling huge closures containing
      Ensemble itself. I think I have fixed this problem.
      The performance numbers may change slightly due to a
      modification of thread_refiner_null, which now composes
      extracts only after an entire proof is done.
      

Changes  Path
+2 -1 metaprl/Makefile
+16 -2 metaprl/clib/Makefile
Added metaprl/clib/extern.c
Properties metaprl/clib/extern.c
Added metaprl/clib/extern.patch
Properties metaprl/clib/extern.patch
Added metaprl/clib/intern.c
Properties metaprl/clib/intern.c
Added metaprl/clib/intern.patch
Properties metaprl/clib/intern.patch
Added metaprl/clib/register.c
Properties metaprl/clib/register.c
Properties metaprl/debug
Added metaprl/debug/Makefile
Properties metaprl/debug/Makefile
Added metaprl/debug/debug.ml
Properties metaprl/debug/debug.ml
Added metaprl/debug/debug.mli
Properties metaprl/debug/debug.mli
Added metaprl/debug/debug_symbols.ml
Properties metaprl/debug/debug_symbols.ml
Added metaprl/debug/debug_symbols.mli
Properties metaprl/debug/debug_symbols.mli
+1 -0 metaprl/editor/ml/.gdbinit
+23 -25 metaprl/editor/ml/Makefile
+1 -1 metaprl/editor/ml/mpconfig
+1 -0 metaprl/editor/ml/shell_mp.ml
+0 -0 metaprl/editor/ml/test.ml
+1 -1 metaprl/editor/ml/w.ml
+0 -1 metaprl/editor/ml/y.ml
+16 -13 metaprl/ensemble/Makefile
+8 -3 metaprl/ensemble/appl_closure.ml
+5 -4 metaprl/ensemble/appl_closure.mli
+49 -6 metaprl/ensemble/ensemble_queue.ml
+32 -17 metaprl/ensemble/remote_ensemble.ml
Added metaprl/ensemble/remote_monitor.ml
Properties metaprl/ensemble/remote_monitor.ml
Added metaprl/ensemble/remote_monitor.mli
Properties metaprl/ensemble/remote_monitor.mli
+21 -5 metaprl/ensemble/remote_null.ml
+9 -5 metaprl/ensemble/remote_sig.mlz
+7 -4 metaprl/ensemble/thread_refiner.mli
+149 -53 metaprl/ensemble/thread_refiner_ens.ml
+7 -4 metaprl/ensemble/thread_refiner_ens.mli
+6 -4 metaprl/ensemble/thread_refiner_ens_mod.ml
+52 -29 metaprl/ensemble/thread_refiner_null.ml
+7 -4 metaprl/ensemble/thread_refiner_null.mli
+6 -4 metaprl/ensemble/thread_refiner_null_mod.ml
+22 -8 metaprl/ensemble/thread_refiner_sig.mlz
+1 -1 metaprl/filter/filter_ast.ml
+1 -1 metaprl/filter/filter_cache.ml
+2 -2 metaprl/mk/config
Properties metaprl/mllib
+3 -2 metaprl/mllib/Makefile
Deleted metaprl/mllib/ctype.ml
Deleted metaprl/mllib/ctype.mli
Added metaprl/mllib/mp_ctype.ml
Properties metaprl/mllib/mp_ctype.ml
Added metaprl/mllib/mp_ctype.mli
Properties metaprl/mllib/mp_ctype.mli
Added metaprl/mllib/register.mlz
Properties metaprl/mllib/register.mlz
+5 -4 metaprl/mllib/remote_lazy_queue.ml
+5 -4 metaprl/mllib/remote_lazy_queue_sig.ml
+30 -12 metaprl/mllib/remote_queue_null.ml
+8 -4 metaprl/mllib/remote_queue_sig.ml
+12 -12 metaprl/refiner/term_ds/term_base_ds.mlp
+14 -14 metaprl/refiner/term_std/term_base_std.mlp
+171 -76 metaprl/theories/tactic/tactic_type.ml
+1 -0 metaprl/theories/tactic/tactic_type.mli
+1 -1 metaprl/theories/tactic/var.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-02 09:04:32 -0800 (Sat, 02 Jan 1999)
Revision: 2551
Log message:

      Fixed some linking problems with intern/extern.c when Ensemble
      is not included.
      

Changes  Path
+8 -3 metaprl/clib/Makefile
+1 -46 metaprl/clib/extern.c
Added metaprl/clib/print_symbols.c
Properties metaprl/clib/print_symbols.c
Added metaprl/clib/print_symbols.h
Properties metaprl/clib/print_symbols.h
+1 -2 metaprl/debug/debug_symbols.ml
+3 -1 metaprl/theories/tactic/tactic_type.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-02 14:23:32 -0800 (Sat, 02 Jan 1999)
Revision: 2552
Log message:

      Fixed the build with undefined OCAMLSRC and the native code build
      

Changes  Path
+6 -0 metaprl/debug/Makefile
+1 -0 metaprl/editor/ml/Makefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-02 21:31:04 -0800 (Sat, 02 Jan 1999)
Revision: 2553
Log message:

      Added profiling control functions stop_gmon and restart_gmon to MP
      top loop. Now it is possible to get a "clean" profiling information
      that does not include any startup overhead.
      

Changes  Path
+1 -0 metaprl/clib/Makefile
+5 -0 metaprl/clib/exit.c
+5 -1 metaprl/editor/ml/shell.ml
+5 -1 metaprl/mk/config

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-02 21:31:36 -0800 (Sat, 02 Jan 1999)
Revision: 2554
Log message:

      Forgot the main profiling file :-)
      

Changes  Path
Added metaprl/clib/profile.c
Properties metaprl/clib/profile.c

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-02 23:24:51 -0800 (Sat, 02 Jan 1999)
Revision: 2555
Log message:

      Another small (~6%) PHP4 speedup
      

Changes  Path
+11 -18 metaprl/refiner/rewrite/rewrite_match_redex.mlp
+10 -13 metaprl/theories/tactic/tactic_type.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-03 00:03:55 -0800 (Sun, 03 Jan 1999)
Revision: 2556
Log message:

      This is a little faster.
      

Changes  Path
+12 -11 metaprl/refiner/refiner/refine.mlp

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-04 16:37:27 -0800 (Mon, 04 Jan 1999)
Revision: 2557
Log message:

      Create ../lib/mbs-mpl.txt link on "make opt"
      

Changes  Path
+1 -1 metaprl/library/Makefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-04 16:52:23 -0800 (Mon, 04 Jan 1999)
Revision: 2558
Log message:

      I've got test.opt to compile, but it would raise an exception when
      I try to run it, probably because I do not know how to
      call Sequent.create
      

Changes  Path
+7 -3 metaprl/theories/itt/Makefile
+3 -5 metaprl/theories/itt/itt_test.ml
+0 -2 metaprl/theories/itt/itt_test.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-04 17:17:51 -0800 (Mon, 04 Jan 1999)
Revision: 2559
Log message:

      Factorial example now works. To run:
      
      % ./mpopt
      # load "itt_test";;
      # cd "itt_test/fact650";;
      # refine timingT factT;;
      

Changes  Path
+0 -47 metaprl/theories/itt/Makefile
+3 -19 metaprl/theories/itt/itt_test.ml
+2 -1 metaprl/theories/itt/itt_test.mli
Deleted metaprl/theories/itt/test.ml
Deleted metaprl/theories/itt/test.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-05 20:11:59 -0800 (Tue, 05 Jan 1999)
Revision: 2560
Log message:

      Test function for itt_fset.
      

Changes  Path
+9 -0 metaprl/theories/itt/itt_fset.ml
+2 -0 metaprl/theories/itt/itt_fset.mli
+6 -0 metaprl/theories/itt/itt_struct.ml
+5 -4 metaprl/theories/itt/itt_struct.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-05 20:12:23 -0800 (Tue, 05 Jan 1999)
Revision: 2561
Log message:

      Test function for refl_term.
      

Changes  Path
+10 -0 metaprl/theories/reflect_itt/refl_term.ml
+2 -0 metaprl/theories/reflect_itt/refl_term.mli

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-01-06 14:28:38 -0800 (Wed, 06 Jan 1999)
Revision: 2562
Log message:

      Added a dash in meta-prl.
      

Changes  Path
+8 -8 metaprl/editor/emacs/prl-hack.el

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-01-06 14:30:39 -0800 (Wed, 06 Jan 1999)
Revision: 2563
Log message:

      Removed redundant opens, indentation fix.
      

Changes  Path
+3 -3 metaprl/refiner/reflib/simple_print.ml
+0 -2 metaprl/refiner/reflib/simple_print.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-08 13:51:02 -0800 (Fri, 08 Jan 1999)
Revision: 2564
Log message:

      This is the version of the distributed prover used in the
      CADE-16 original paper.  I'm still adjusting it though, so
      that we can use term_ds and native-code.
      
      If any of you have problems compiling clib/mmap.c, let me know.  It
      should compile on Linux and Win32, but we should put in stubs
      if there are problems on other systems.
      

Changes  Path
+4 -3 metaprl/clib/Makefile
+17 -0 metaprl/clib/extern.c
Added metaprl/clib/inextern.h
Properties metaprl/clib/inextern.h
+12 -0 metaprl/clib/intern.c
Added metaprl/clib/mmap.c
Properties metaprl/clib/mmap.c
Added metaprl/clib/mmap.h
Properties metaprl/clib/mmap.h
+1 -1 metaprl/clib/print_symbols.c
+1 -0 metaprl/clib/print_symbols.h
+9 -4 metaprl/clib/register.c
+3 -4 metaprl/editor/ml/Makefile
+3 -2 metaprl/editor/ml/mpconfig
Added metaprl/editor/ml/mpserver
Properties metaprl/editor/ml/mpserver
+15 -2 metaprl/editor/ml/test.ml
+1 -0 metaprl/editor/ml/w.ml
+2 -1 metaprl/editor/ml/y.ml
+51 -2 metaprl/ensemble/Makefile
Added metaprl/ensemble/appl_ensemble.ml
Properties metaprl/ensemble/appl_ensemble.ml
Added metaprl/ensemble/appl_ensemble.mli
Properties metaprl/ensemble/appl_ensemble.mli
Added metaprl/ensemble/appl_outboard_client.ml
Properties metaprl/ensemble/appl_outboard_client.ml
Added metaprl/ensemble/appl_outboard_client.mli
Properties metaprl/ensemble/appl_outboard_client.mli
Added metaprl/ensemble/appl_outboard_common.ml
Properties metaprl/ensemble/appl_outboard_common.ml
Added metaprl/ensemble/appl_outboard_common.mli
Properties metaprl/ensemble/appl_outboard_common.mli
Added metaprl/ensemble/appl_outboard_server.ml
Properties metaprl/ensemble/appl_outboard_server.ml
Added metaprl/ensemble/appl_outboard_server.mli
Properties metaprl/ensemble/appl_outboard_server.mli
+621 -347 metaprl/ensemble/ensemble_queue.ml
+30 -12 metaprl/ensemble/remote_ensemble.ml
+23 -19 metaprl/ensemble/thread_refiner_ens.ml
+1 -1 metaprl/mk/config
+4 -1 metaprl/mllib/Makefile
Added metaprl/mllib/mmap.ml
Properties metaprl/mllib/mmap.ml
Added metaprl/mllib/mmap.mli
Properties metaprl/mllib/mmap.mli
Added metaprl/mllib/mmap_pipe.ml
Properties metaprl/mllib/mmap_pipe.ml
Added metaprl/mllib/mmap_pipe.mli
Properties metaprl/mllib/mmap_pipe.mli
+1 -1 metaprl/mllib/register.mlz
+5 -5 metaprl/refiner/refiner/refiner.ml
+2 -2 metaprl/theories/tactic/tactic_type.ml
+1 -1 metaprl/theories/tptp/tptp_prove.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-09 17:51:16 -0800 (Sat, 09 Jan 1999)
Revision: 2565
Log message:

      Fixed misleading comment
      

Changes  Path
+6 -2 metaprl/refiner/term_ds/term_ds_sig.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-12 14:36:39 -0800 (Tue, 12 Jan 1999)
Revision: 2566
Log message:

      Set LC_ALL and LANG environment variables to "C" when creating
      mp_version.ml, so that the date in mp_version would always be in English
      

Changes  Path
+2 -2 metaprl/editor/ml/Makefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-12 15:10:22 -0800 (Tue, 12 Jan 1999)
Revision: 2567
Log message:

      Suffix for the Refiner module to use.
      Possible values: ds_verb, ds_simp, std_verb, std_simp
      
      The system looks for suffix to use:
       1) In .refiner file (if it's non-empty)
       2) In MP_REFINER environment variable (if set)
       3) Prints warning and uses "ds_verb"
      

Changes  Path
Properties metaprl/refiner/refiner
+27 -0 metaprl/refiner/refiner/Makefile
Deleted metaprl/refiner/refiner/refiner.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-14 11:36:37 -0800 (Thu, 14 Jan 1999)
Revision: 2568
Log message:

      I believe, I've fixed the problem Yegor had found.
      
      The bug was not in == comparisons, but in compare_params
      function, where some indices were wrong.
      

Changes  Path
+8 -8 metaprl/refiner/reflib/term_copy.ml

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 1999-01-15 02:00:56 -0800 (Fri, 15 Jan 1999)
Revision: 2569
Log message:

      
      CVS:
      

Changes  Path
+1 -1 metaprl/mllib/bi_memo.ml
+2 -2 metaprl/mllib/simplehashtbl.ml
+9 -9 metaprl/refiner/reflib/term_compare.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-15 16:43:16 -0800 (Fri, 15 Jan 1999)
Revision: 2570
Log message:

      Added smaller examples.
      

Changes  Path
+10 -4 metaprl/theories/itt/itt_test.ml
+6 -4 metaprl/theories/itt/itt_test.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-16 18:28:45 -0800 (Sat, 16 Jan 1999)
Revision: 2571
Log message:

      A Quick Guide to MetaPRL Profiling
      

Changes  Path
Added metaprl/doc/profiling.txt
Properties metaprl/doc/profiling.txt

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 1999-01-17 00:09:25 -0800 (Sun, 17 Jan 1999)
Revision: 2572
Log message:

      
      
      Alternate version of Term_copy with Alesha'a "fast" algorithm.
      Not tested yet.
      

Changes  Path
Added metaprl/mllib/ar_memo.ml
Properties metaprl/mllib/ar_memo.ml
Added metaprl/mllib/ar_memo.mli
Properties metaprl/mllib/ar_memo.mli
Added metaprl/mllib/infinite_ro_array.ml
Properties metaprl/mllib/infinite_ro_array.ml
Added metaprl/mllib/infinite_ro_array.mli
Properties metaprl/mllib/infinite_ro_array.mli
Added metaprl/mllib/infinite_ro_array_sig.mlz
Properties metaprl/mllib/infinite_ro_array_sig.mlz
Added metaprl/refiner/reflib/ar_term_copy.ml
Properties metaprl/refiner/reflib/ar_term_copy.ml
Added metaprl/refiner/reflib/ar_term_copy.mli
Properties metaprl/refiner/reflib/ar_term_copy.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-25 10:21:31 -0800 (Mon, 25 Jan 1999)
Revision: 2573
Log message:

      Distributed refiner for CADE-16.
      

Changes  Path
+9 -6 metaprl/clib/Makefile
+16 -34 metaprl/editor/ml/Makefile
+1 -1 metaprl/editor/ml/mpconfig
+5 -11 metaprl/editor/ml/test.ml
+9 -3 metaprl/ensemble/Makefile
+5 -0 metaprl/ensemble/appl_outboard_server.ml
+1 -0 metaprl/ensemble/ensemble_queue.ml
+2 -2 metaprl/ensemble/remote_ensemble.ml
+1 -1 metaprl/ensemble/remote_null.ml
+1 -1 metaprl/ensemble/remote_sig.mlz
+19 -9 metaprl/ensemble/thread_refiner_ens.ml
+17 -12 metaprl/filter/Makefile
+18 -8 metaprl/mk/config
+3 -1 metaprl/theories/itt/itt_bool.ml
+8 -0 metaprl/theories/itt/itt_int.ml
+9 -1 metaprl/theories/itt/itt_int_bool.ml
+5 -5 metaprl/theories/itt/itt_int_bool.mli
+2 -1 metaprl/theories/itt/itt_rfun.ml
+15 -11 metaprl/theories/itt/itt_test.ml
+6 -19 metaprl/theories/ocaml_sos/Makefile
+23 -32 metaprl/theories/ocaml_sos/ocaml_base_sos.ml
+19 -12 metaprl/theories/ocaml_sos/ocaml_base_sos.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-25 10:34:13 -0800 (Mon, 25 Jan 1999)
Revision: 2574
Log message:

      Added edit_set_goal, which loads the package if it is not yet loaded.
      

Changes  Path
+1 -1 metaprl/editor/ml/Makefile
+5 -0 metaprl/editor/ml/mp.ml
+5 -0 metaprl/editor/ml/mp.mli
+18 -0 metaprl/editor/ml/shell.ml
+5 -0 metaprl/editor/ml/shell.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-25 11:23:08 -0800 (Mon, 25 Jan 1999)
Revision: 2575
Log message:

      Added edit_save function to save a specific package.
      

Changes  Path
+2 -0 metaprl/editor/ml/shell.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-27 19:57:07 -0800 (Wed, 27 Jan 1999)
Revision: 2576
Log message:

      Added some simple code to match two hypothesis lists.
      It does not always do the right thing, but would probably
      succeed in many cases
      

Changes  Path
+2 -1 metaprl/refiner/reflib/Files
Added metaprl/refiner/reflib/match_seq.ml
Properties metaprl/refiner/reflib/match_seq.ml
Added metaprl/refiner/reflib/match_seq.mli
Properties metaprl/refiner/reflib/match_seq.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-28 10:44:05 -0800 (Thu, 28 Jan 1999)
Revision: 2577
Log message:

      Upgraded to OCaml 2.01.
      

Changes  Path
+56 -63 metaprl/editor/ml/library_eval.ml
+2 -2 metaprl/editor/ml/package_info.ml
+15 -15 metaprl/editor/ml/shell.ml
+7 -7 metaprl/editor/ml/shell_p4.ml
+4 -4 metaprl/ensemble/appl_outboard_client.ml
+1 -1 metaprl/ensemble/appl_outboard_server.ml
+6 -6 metaprl/filter/filter_cache_fun.ml
+19 -19 metaprl/filter/filter_comment.ml
+25 -19 metaprl/filter/filter_hash.ml
+64 -35 metaprl/filter/filter_ocaml.ml
+8 -8 metaprl/filter/filter_ocaml.mli
+32 -26 metaprl/filter/mLast_util.ml
+6 -6 metaprl/filter/mLast_util.mli
+1 -1 metaprl/library/library_type_base.ml
+6 -6 metaprl/refiner/refiner/refine.mlp
+3 -3 metaprl/refiner/refsig/refine_sig.ml
+4 -1 metaprl/theories/tactic/mptop.ml
+11 -11 metaprl/theories/tactic/tactic_cache.ml
+4 -4 metaprl/theories/tactic/tactic_type.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-01-28 14:53:13 -0800 (Thu, 28 Jan 1999)
Revision: 2578
Log message:

      Fixed some of "this expression should have type unit" warnings
      

Changes  Path
+1 -2 metaprl/filter/filter_main.ml
+2 -2 metaprl/filter/filter_parse.ml
+1 -2 metaprl/filter/prlcomp.ml
+10 -5 metaprl/mllib/mmap_pipe.ml
+4 -1 metaprl/mllib/punix.ml
+1 -1 metaprl/mllib/punix.mli
+2 -2 metaprl/refiner/term_ds/term_man_ds.mlp
+4 -3 metaprl/theories/itt/itt_logic.ml

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 1999-01-29 09:26:07 -0800 (Fri, 29 Jan 1999)
Revision: 2579
Log message:

      Upgraded to OCaml 2.01.
      

Changes  Path
+165 -149 metaprl/editor/ml/library_eval.ml
+34 -21 metaprl/editor/ml/library_test.ml
+2 -2 metaprl/library/library.mli
+18 -19 metaprl/library/library_type_base.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-31 13:42:08 -0800 (Sun, 31 Jan 1999)
Revision: 2580
Log message:

      Added "simp" and "verb" rules to Makefiles.  There are no *.mlp and *.mlip
      files in the refiner any longer.  Instead, the C-preprocessor is run at
      compile time.
      
      By default, the verbose refiner is generated.  To get the others, use
      make simp, or make opt_simp.
      

Changes  Path
+32 -15 metaprl/Makefile
Binary metaprl/editor/emacs/caml-fa.elc
Properties metaprl/editor/emacs/caml-fa.elc
Binary metaprl/editor/emacs/caml-util.elc
Properties metaprl/editor/emacs/caml-util.elc
Binary metaprl/editor/emacs/caml.elc
Properties metaprl/editor/emacs/caml.elc
+1 -1 metaprl/editor/ml/proof.ml
+1 -1 metaprl/editor/ml/proof.mli
+8 -8 metaprl/filter/filter_cache.ml
+40 -33 metaprl/mk/config
+24 -12 metaprl/mk/preface
+3 -8 metaprl/refiner/refiner/Files
+12 -11 metaprl/refiner/refiner/Makefile
Added metaprl/refiner/refiner/refine.ml
Properties metaprl/refiner/refiner/refine.ml
Added metaprl/refiner/refiner/refine.mli
Properties metaprl/refiner/refiner/refine.mli
Deleted metaprl/refiner/refiner/refine.mlip
Deleted metaprl/refiner/refiner/refine.mlp
Added metaprl/refiner/refiner/refiner_ds.ml
Properties metaprl/refiner/refiner/refiner_ds.ml
Added metaprl/refiner/refiner/refiner_ds.mli
Properties metaprl/refiner/refiner/refiner_ds.mli
Deleted metaprl/refiner/refiner/refiner_ds_simp.ml
Deleted metaprl/refiner/refiner/refiner_ds_simp.mli
Deleted metaprl/refiner/refiner/refiner_ds_verb.ml
Deleted metaprl/refiner/refiner/refiner_ds_verb.mli
Added metaprl/refiner/refiner/refiner_std.ml
Properties metaprl/refiner/refiner/refiner_std.ml
Added metaprl/refiner/refiner/refiner_std.mli
Properties metaprl/refiner/refiner/refiner_std.mli
Deleted metaprl/refiner/refiner/refiner_std_simp.ml
Deleted metaprl/refiner/refiner/refiner_std_simp.mli
Deleted metaprl/refiner/refiner/refiner_std_verb.ml
Deleted metaprl/refiner/refiner/refiner_std_verb.mli
+4 -4 metaprl/refiner/reflib/Files
+6 -6 metaprl/refiner/reflib/ml_term.ml
+6 -6 metaprl/refiner/reflib/term_copy.ml
+12 -12 metaprl/refiner/reflib/term_copy.mli
+5 -5 metaprl/refiner/reflib/term_copy2.ml
+12 -12 metaprl/refiner/reflib/term_copy2.mli
+7 -3 metaprl/refiner/refsig/refine_error.h
+9 -12 metaprl/refiner/rewrite/Files
+2 -0 metaprl/refiner/rewrite/Makefile
Added metaprl/refiner/rewrite/rewrite.ml
Properties metaprl/refiner/rewrite/rewrite.ml
Added metaprl/refiner/rewrite/rewrite.mli
Properties metaprl/refiner/rewrite/rewrite.mli
Deleted metaprl/refiner/rewrite/rewrite.mlip
Deleted metaprl/refiner/rewrite/rewrite.mlp
Added metaprl/refiner/rewrite/rewrite_build_contractum.ml
Properties metaprl/refiner/rewrite/rewrite_build_contractum.ml
Added metaprl/refiner/rewrite/rewrite_build_contractum.mli
Properties metaprl/refiner/rewrite/rewrite_build_contractum.mli
Deleted metaprl/refiner/rewrite/rewrite_build_contractum.mlip
Deleted metaprl/refiner/rewrite/rewrite_build_contractum.mlp
Added metaprl/refiner/rewrite/rewrite_compile_contractum.ml
Properties metaprl/refiner/rewrite/rewrite_compile_contractum.ml
Added metaprl/refiner/rewrite/rewrite_compile_contractum.mli
Properties metaprl/refiner/rewrite/rewrite_compile_contractum.mli
Deleted metaprl/refiner/rewrite/rewrite_compile_contractum.mlip
Deleted metaprl/refiner/rewrite/rewrite_compile_contractum.mlp
Added metaprl/refiner/rewrite/rewrite_compile_redex.ml
Properties metaprl/refiner/rewrite/rewrite_compile_redex.ml
Added metaprl/refiner/rewrite/rewrite_compile_redex.mli
Properties metaprl/refiner/rewrite/rewrite_compile_redex.mli
Deleted metaprl/refiner/rewrite/rewrite_compile_redex.mlip
Deleted metaprl/refiner/rewrite/rewrite_compile_redex.mlp
Added metaprl/refiner/rewrite/rewrite_debug.ml
Properties metaprl/refiner/rewrite/rewrite_debug.ml
Added metaprl/refiner/rewrite/rewrite_debug.mli
Properties metaprl/refiner/rewrite/rewrite_debug.mli
Deleted metaprl/refiner/rewrite/rewrite_debug.mlip
Deleted metaprl/refiner/rewrite/rewrite_debug.mlp
Added metaprl/refiner/rewrite/rewrite_match_redex.ml
Properties metaprl/refiner/rewrite/rewrite_match_redex.ml
Added metaprl/refiner/rewrite/rewrite_match_redex.mli
Properties metaprl/refiner/rewrite/rewrite_match_redex.mli
Deleted metaprl/refiner/rewrite/rewrite_match_redex.mlip
Deleted metaprl/refiner/rewrite/rewrite_match_redex.mlp
Added metaprl/refiner/rewrite/rewrite_meta.ml
Properties metaprl/refiner/rewrite/rewrite_meta.ml
Added metaprl/refiner/rewrite/rewrite_meta.mli
Properties metaprl/refiner/rewrite/rewrite_meta.mli
Deleted metaprl/refiner/rewrite/rewrite_meta.mlip
Deleted metaprl/refiner/rewrite/rewrite_meta.mlp
Deleted metaprl/refiner/rewrite/rewrite_type.mlip
Deleted metaprl/refiner/rewrite/rewrite_type.mlp
Added metaprl/refiner/rewrite/rewrite_types.ml
Properties metaprl/refiner/rewrite/rewrite_types.ml
Added metaprl/refiner/rewrite/rewrite_types.mli
Properties metaprl/refiner/rewrite/rewrite_types.mli
Added metaprl/refiner/rewrite/rewrite_util.ml
Properties metaprl/refiner/rewrite/rewrite_util.ml
Added metaprl/refiner/rewrite/rewrite_util.mli
Properties metaprl/refiner/rewrite/rewrite_util.mli
Deleted metaprl/refiner/rewrite/rewrite_util.mlip
Deleted metaprl/refiner/rewrite/rewrite_util.mlp
+3 -6 metaprl/refiner/term_ds/Files
+2 -0 metaprl/refiner/term_ds/Makefile
Added metaprl/refiner/term_ds/term_addr_ds.ml
Properties metaprl/refiner/term_ds/term_addr_ds.ml
Added metaprl/refiner/term_ds/term_addr_ds.mli
Properties metaprl/refiner/term_ds/term_addr_ds.mli
Deleted metaprl/refiner/term_ds/term_addr_ds.mlip
Deleted metaprl/refiner/term_ds/term_addr_ds.mlp
Added metaprl/refiner/term_ds/term_base_ds.ml
Properties metaprl/refiner/term_ds/term_base_ds.ml
Added metaprl/refiner/term_ds/term_base_ds.mli
Properties metaprl/refiner/term_ds/term_base_ds.mli
Deleted metaprl/refiner/term_ds/term_base_ds.mlip
Deleted metaprl/refiner/term_ds/term_base_ds.mlp
Added metaprl/refiner/term_ds/term_eval_ds.ml
Properties metaprl/refiner/term_ds/term_eval_ds.ml
Added metaprl/refiner/term_ds/term_eval_ds.mli
Properties metaprl/refiner/term_ds/term_eval_ds.mli
Deleted metaprl/refiner/term_ds/term_eval_ds.mlip
Deleted metaprl/refiner/term_ds/term_eval_ds.mlp
Added metaprl/refiner/term_ds/term_man_ds.ml
Properties metaprl/refiner/term_ds/term_man_ds.ml
Added metaprl/refiner/term_ds/term_man_ds.mli
Properties metaprl/refiner/term_ds/term_man_ds.mli
Deleted metaprl/refiner/term_ds/term_man_ds.mlip
Deleted metaprl/refiner/term_ds/term_man_ds.mlp
Added metaprl/refiner/term_ds/term_op_ds.ml
Properties metaprl/refiner/term_ds/term_op_ds.ml
Added metaprl/refiner/term_ds/term_op_ds.mli
Properties metaprl/refiner/term_ds/term_op_ds.mli
Deleted metaprl/refiner/term_ds/term_op_ds.mlip
Deleted metaprl/refiner/term_ds/term_op_ds.mlp
Added metaprl/refiner/term_ds/term_subst_ds.ml
Properties metaprl/refiner/term_ds/term_subst_ds.ml
Added metaprl/refiner/term_ds/term_subst_ds.mli
Properties metaprl/refiner/term_ds/term_subst_ds.mli
Deleted metaprl/refiner/term_ds/term_subst_ds.mlip
Deleted metaprl/refiner/term_ds/term_subst_ds.mlp
+1 -4 metaprl/refiner/term_gen/Files
+2 -0 metaprl/refiner/term_gen/Makefile
Added metaprl/refiner/term_gen/term_addr_gen.ml
Properties metaprl/refiner/term_gen/term_addr_gen.ml
Added metaprl/refiner/term_gen/term_addr_gen.mli
Properties metaprl/refiner/term_gen/term_addr_gen.mli
Deleted metaprl/refiner/term_gen/term_addr_gen.mlip
Deleted metaprl/refiner/term_gen/term_addr_gen.mlp
Added metaprl/refiner/term_gen/term_man_gen.ml
Properties metaprl/refiner/term_gen/term_man_gen.ml
Added metaprl/refiner/term_gen/term_man_gen.mli
Properties metaprl/refiner/term_gen/term_man_gen.mli
Deleted metaprl/refiner/term_gen/term_man_gen.mlip
Deleted metaprl/refiner/term_gen/term_man_gen.mlp
Added metaprl/refiner/term_gen/term_meta_gen.ml
Properties metaprl/refiner/term_gen/term_meta_gen.ml
Added metaprl/refiner/term_gen/term_meta_gen.mli
Properties metaprl/refiner/term_gen/term_meta_gen.mli
Deleted metaprl/refiner/term_gen/term_meta_gen.mlip
Deleted metaprl/refiner/term_gen/term_meta_gen.mlp
Added metaprl/refiner/term_gen/term_shape_gen.ml
Properties metaprl/refiner/term_gen/term_shape_gen.ml
Added metaprl/refiner/term_gen/term_shape_gen.mli
Properties metaprl/refiner/term_gen/term_shape_gen.mli
Deleted metaprl/refiner/term_gen/term_shape_gen.mlip
Deleted metaprl/refiner/term_gen/term_shape_gen.mlp
+3 -6 metaprl/refiner/term_std/Files
+2 -0 metaprl/refiner/term_std/Makefile
Added metaprl/refiner/term_std/term_base_std.ml
Properties metaprl/refiner/term_std/term_base_std.ml
Added metaprl/refiner/term_std/term_base_std.mli
Properties metaprl/refiner/term_std/term_base_std.mli
Deleted metaprl/refiner/term_std/term_base_std.mlip
Deleted metaprl/refiner/term_std/term_base_std.mlp
Added metaprl/refiner/term_std/term_eval_std.ml
Properties metaprl/refiner/term_std/term_eval_std.ml
Added metaprl/refiner/term_std/term_eval_std.mli
Properties metaprl/refiner/term_std/term_eval_std.mli
Deleted metaprl/refiner/term_std/term_eval_std.mlip
Deleted metaprl/refiner/term_std/term_eval_std.mlp
Added metaprl/refiner/term_std/term_op_std.ml
Properties metaprl/refiner/term_std/term_op_std.ml
Added metaprl/refiner/term_std/term_op_std.mli
Properties metaprl/refiner/term_std/term_op_std.mli
Deleted metaprl/refiner/term_std/term_op_std.mlip
Deleted metaprl/refiner/term_std/term_op_std.mlp
Added metaprl/refiner/term_std/term_subst_std.ml
Properties metaprl/refiner/term_std/term_subst_std.ml
Added metaprl/refiner/term_std/term_subst_std.mli
Properties metaprl/refiner/term_std/term_subst_std.mli
Deleted metaprl/refiner/term_std/term_subst_std.mlip
Deleted metaprl/refiner/term_std/term_subst_std.mlp