Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-04-03 21:24:42 -0800 (Sat, 03 Apr 1999)
Revision: 2626
Log message:

      Added MetaLabeled of string * meta_term variant to meta_term type
      
      Ml_format.print_term would raise an exception when given meta_term -
      I could not figure out what is supposed to go there.
      
      In filter_simmary in functions meta_term_of_term and term_of_meta_term
      MetaLabeled (l, t) is encoded as   meta_labeled [String l] (t)
      

Changes  Path
+15 -1 metaprl/filter/filter_summary.ml
+40 -35 metaprl/refiner/reflib/dform.ml
+3 -0 metaprl/refiner/reflib/ml_format.ml
+39 -35 metaprl/refiner/reflib/simple_print.ml
+2 -0 metaprl/refiner/refsig/term_header_sig.mlz
+1 -0 metaprl/refiner/refsig/term_simple_sig.mlz
+1 -0 metaprl/refiner/term_ds/term_ds.ml
+1 -0 metaprl/refiner/term_ds/term_ds_sig.ml
+2 -0 metaprl/refiner/term_gen/term_hash.ml
+4 -0 metaprl/refiner/term_gen/term_header.ml
+2 -0 metaprl/refiner/term_gen/term_header_constr.ml
+34 -21 metaprl/refiner/term_gen/term_meta_gen.ml
+2 -0 metaprl/refiner/term_std/term_std.ml
+1 -0 metaprl/refiner/term_std/term_std_sig.ml