Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-03 15:20:09 -0700 (Wed, 03 Jun 1998)
Revision: 2216
Log message:

      Nonpolymorphic refiner.
      

Changes	Path
+1 -0	metaprl/clib/Makefile
Added	metaprl/clib/execvp.c
Properties	metaprl/clib/execvp.c
+5 -0	metaprl/clib/punix.ml
+8 -0	metaprl/clib/punix.mli
+20 -50	metaprl/editor/ml/io_proof.ml
+10 -6	metaprl/editor/ml/io_proof_type.mlz
+30 -30	metaprl/editor/ml/proof.ml
+8 -4	metaprl/editor/ml/proof_edit.ml
+28 -27	metaprl/editor/ml/proof_step.ml
+7 -9	metaprl/editor/ml/shell_rewrite.ml
+20 -9	metaprl/filter/filter_prog.ml
+4 -1	metaprl/filter/prlcomp.ml
+16 -0	metaprl/mllib/list_util.ml
+4 -0	metaprl/mllib/list_util.mli
+4 -1	metaprl/refiner/refiner/refiner_ds.ml
+4 -1	metaprl/refiner/refiner/refiner_std.ml
+6 -2	metaprl/refiner/refsig/refiner_sig.ml
+9 -6	metaprl/refiner/refsig/term_addr_sig.ml
+13 -3	metaprl/refiner/refsig/term_man_sig.ml
+14 -0	metaprl/refiner/refsig/term_simple_sig.mlz
+3 -0	metaprl/refiner/term_ds/term_ds.ml
+1 -0	metaprl/refiner/term_ds/term_ds.mli
+12 -13	metaprl/refiner/term_gen/term_addr_gen.ml
+285 -155	metaprl/refiner/term_gen/term_man_gen.ml
+7 -0	metaprl/refiner/term_gen/term_man_gen.mli
+6 -2	metaprl/refiner/term_std/term_std.ml
+4 -0	metaprl/refiner/term_std/term_std.mli
+6 -3	metaprl/theories/base/base_cache.ml
+6 -3	metaprl/theories/base/base_cache.mli
+6 -1	metaprl/theories/base/typeinf.ml
+6 -1	metaprl/theories/itt/itt_equal.ml
+9 -11	metaprl/theories/itt/itt_soft.ml
+4 -1	metaprl/theories/itt/itt_soft.mli
+8 -3	metaprl/theories/itt/itt_squash.ml
+6 -1	metaprl/theories/itt/itt_subtype.ml
+4 -5	metaprl/theories/tactic/Makefile
Added	metaprl/theories/tactic/conversionals.ml
Properties	metaprl/theories/tactic/conversionals.ml
Added	metaprl/theories/tactic/conversionals.mli
Properties	metaprl/theories/tactic/conversionals.mli
Added	metaprl/theories/tactic/rewrite_type.ml
Properties	metaprl/theories/tactic/rewrite_type.ml
Added	metaprl/theories/tactic/rewrite_type.mli
Properties	metaprl/theories/tactic/rewrite_type.mli
+45 -22	metaprl/theories/tactic/sequent.ml
+26 -17	metaprl/theories/tactic/sequent.mli
Added	metaprl/theories/tactic/tactic_type.ml
Properties	metaprl/theories/tactic/tactic_type.ml
Added	metaprl/theories/tactic/tactic_type.mli
Properties	metaprl/theories/tactic/tactic_type.mli
Deleted	metaprl/theories/tactic/tactic_type.mlz
+62 -96	metaprl/theories/tactic/tacticals.ml
+32 -29	metaprl/theories/tactic/tacticals.mli
+22 -20	metaprl/theories/tactic/var.ml
+9 -7	metaprl/theories/tactic/var.mli
+11 -2	metaprl/util/ocamldep.mll