Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-07 18:58:47 -0700 (Mon, 07 Jul 2003)
Revision: 4714
Log message:

      - Added Lm-symbol.make that takes an explicit string and an int.
      - The meta-sequent labels are strings, not variables.
      

Changes  Path
+4 -8 metaprl-branches/abstract_vars/editor/ml/Makefile
+2 -2 metaprl-branches/abstract_vars/filter/Makefile
+3 -2 metaprl-branches/abstract_vars/filter/base/filter_cache.ml
+3 -3 metaprl-branches/abstract_vars/filter/base/filter_summary.ml
+2 -2 metaprl-branches/abstract_vars/filter/base/filter_util.ml
+1 -1 metaprl-branches/abstract_vars/filter/base/filter_util.mli
+2 -4 metaprl-branches/abstract_vars/filter/filter/filter_parse.ml
+0 -1 metaprl-branches/abstract_vars/filter/filter/filter_prog.ml
+0 -2 metaprl-branches/abstract_vars/filter/filter/term_grammar.ml
+1 -1 metaprl-branches/abstract_vars/refiner/reflib/dform.ml
+1 -1 metaprl-branches/abstract_vars/refiner/reflib/simple_print.ml
+1 -1 metaprl-branches/abstract_vars/refiner/refsig/term_hash_sig.ml
+1 -1 metaprl-branches/abstract_vars/refiner/refsig/term_meta_sig.ml
+1 -1 metaprl-branches/abstract_vars/refiner/refsig/term_sig.ml
+1 -1 metaprl-branches/abstract_vars/refiner/term_ds/term_ds.ml
+1 -1 metaprl-branches/abstract_vars/refiner/term_ds/term_ds_sig.ml
+2 -2 metaprl-branches/abstract_vars/refiner/term_gen/term_hash.ml
+1 -1 metaprl-branches/abstract_vars/refiner/term_std/term_std.ml
+1 -1 metaprl-branches/abstract_vars/refiner/term_std/term_std_sig.ml