Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-18 14:04:59 -0700 (Fri, 18 Jul 2003)
Revision: 4759
Log message:

      Added sequent support to pattern matching and explode_term.
      explode_term has moved to TermMan, to add support for sequents.
      

Changes  Path
+57 -3 metaprl/filter/filter/filter_patt.ml
+1 -1 metaprl/refiner/refsig/refiner_sig.ml
+0 -10 metaprl/refiner/refsig/term_base_sig.ml
+8 -0 metaprl/refiner/refsig/term_man_sig.ml
+19 -13 metaprl/refiner/refsig/term_sig.ml
+0 -34 metaprl/refiner/term_ds/term_base_ds.ml
+0 -1 metaprl/refiner/term_ds/term_base_ds.mli
+16 -13 metaprl/refiner/term_ds/term_ds.ml
+16 -18 metaprl/refiner/term_ds/term_ds_sig.ml
+41 -0 metaprl/refiner/term_ds/term_man_ds.ml
+1 -0 metaprl/refiner/term_ds/term_man_ds.mli
+44 -0 metaprl/refiner/term_gen/term_man_gen.ml
+5 -4 metaprl/refiner/term_gen/term_man_gen.mli
+0 -26 metaprl/refiner/term_std/term_base_std.ml
+0 -1 metaprl/refiner/term_std/term_base_std.mli
+16 -13 metaprl/refiner/term_std/term_std.ml
+16 -18 metaprl/refiner/term_std/term_std_sig.ml
+1 -1 metaprl/theories/base/base_meta.ml