Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-23 19:03:44 -0800 (Sun, 23 Jan 2005)
Revision: 6479
Log message:

      Separated tokens from normal terms.
      
      The final thing to do is get mmc to compile, then we should merge.
      

Changes  Path
+140 -90 metaprl-branches/opname_classes2/filter/base/filter_cache_fun.ml
+1 -0 metaprl-branches/opname_classes2/filter/base/filter_summary_type.ml
+12 -5 metaprl-branches/opname_classes2/filter/base/filter_type.ml
+5 -5 metaprl-branches/opname_classes2/filter/filter/filter_parse.ml
+5 -4 metaprl-branches/opname_classes2/filter/filter/term_grammar.ml
+16 -8 metaprl-branches/opname_classes2/refiner/refbase/opname.ml
+4 -3 metaprl-branches/opname_classes2/refiner/refbase/opname.mli
+1 -0 metaprl-branches/opname_classes2/refiner/refsig/term_op_sig.ml
+5 -0 metaprl-branches/opname_classes2/refiner/term_ds/term_op_ds.ml
+5 -0 metaprl-branches/opname_classes2/refiner/term_std/term_op_std.ml
+2 -2 metaprl-branches/opname_classes2/support/shell/package_info.ml
+5 -5 metaprl-branches/opname_classes2/support/shell/package_info.mli
+2 -2 metaprl-branches/opname_classes2/support/shell/shell_core.ml
+8 -8 metaprl-branches/opname_classes2/support/shell/shell_state.ml
+1 -1 metaprl-branches/opname_classes2/support/shell/shell_state.mli
+2 -1 metaprl-branches/opname_classes2/theories/itt/itt_grouplikeobj.ml
+2 -1 metaprl-branches/opname_classes2/theories/itt/itt_ring2.ml