Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-18 22:36:02 -0800 (Tue, 18 Mar 2003)
Revision: 4185
Log message:

      - I moved the sequent-related *_addr functions from TermMan to TermAddr
      - I got rid of the TermSimleSig signature, use TermSig instead
      - The Lib_term module now uses the Term_man_gen for converting
      from/to term representation of sequents instead of reimplementing it.
      

Changes  Path
+2 -6 metaprl/filter/base/filter_ocaml.ml
+2 -6 metaprl/filter/boot/proof_term_boot.ml
+2 -2 metaprl/filter/boot/sequent_boot.ml
+4 -8 metaprl/filter/phobos/phobos_constants.ml
+1 -1 metaprl/library/db.ml
+6 -120 metaprl/library/lib_term.ml
+1 -1 metaprl/refiner/refiner/refiner_ds.ml
+2 -2 metaprl/refiner/refiner/refiner_std.ml
+0 -1 metaprl/refiner/refsig/Files
+0 -17 metaprl/refiner/refsig/Makefile
+0 -1 metaprl/refiner/refsig/refiner_sig.ml
+10 -0 metaprl/refiner/refsig/term_addr_sig.ml
+1 -0 metaprl/refiner/refsig/term_base_sig.ml
+1 -12 metaprl/refiner/refsig/term_man_sig.ml
Added metaprl/refiner/refsig/term_sig.ml
Properties metaprl/refiner/refsig/term_sig.ml
Deleted metaprl/refiner/refsig/term_simple_sig.mlz
+56 -0 metaprl/refiner/term_ds/term_addr_ds.ml
+1 -0 metaprl/refiner/term_ds/term_base_ds.ml
+1 -0 metaprl/refiner/term_ds/term_ds_sig.ml
+1 -64 metaprl/refiner/term_ds/term_man_ds.ml
+1 -7 metaprl/refiner/term_ds/term_man_ds.mli
+2 -1 metaprl/refiner/term_gen/Files
+1 -0 metaprl/refiner/term_gen/Makefile
+107 -0 metaprl/refiner/term_gen/term_addr_gen.ml
+4 -7 metaprl/refiner/term_gen/term_addr_gen.mli
+126 -261 metaprl/refiner/term_gen/term_man_gen.ml
+13 -11 metaprl/refiner/term_gen/term_man_gen.mli
Added metaprl/refiner/term_gen/term_man_gen_sig.ml
Properties metaprl/refiner/term_gen/term_man_gen_sig.ml
+7 -5 metaprl/refiner/term_gen/term_shape_gen.ml
+4 -2 metaprl/refiner/term_gen/term_shape_gen.mli
+1 -0 metaprl/refiner/term_std/term_base_std.ml
+1 -0 metaprl/refiner/term_std/term_std_sig.ml
+2 -2 metaprl/theories/base/base_meta.ml
+1 -3 metaprl/theories/fir/mfir_termOp_base.ml