Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-16 19:48:54 -0800 (Sun, 16 Jan 2005)
Revision: 6415
Log message:

      This branch views the token parameter as an opname (see bug #370),
      with rudimentary support for opname classes.
      

Changes  Path
+54 -52 metaprl-branches/opname_classes/editor/ml/nuprl_eval.ml
+3 -1 metaprl-branches/opname_classes/editor/ml/nuprl_jprover.ml
+180 -26 metaprl-branches/opname_classes/filter/base/filter_cache_fun.ml
+1 -1 metaprl-branches/opname_classes/filter/base/filter_magic.ml
+243 -42 metaprl-branches/opname_classes/filter/base/filter_summary.ml
+4 -1 metaprl-branches/opname_classes/filter/base/filter_summary_type.ml
+5 -0 metaprl-branches/opname_classes/filter/base/filter_type.ml
+73 -34 metaprl-branches/opname_classes/filter/filter/filter_parse.ml
+2 -2 metaprl-branches/opname_classes/filter/filter/filter_patt.ml
+10 -2 metaprl-branches/opname_classes/filter/filter/filter_prog.ml
+17 -16 metaprl-branches/opname_classes/filter/filter/term_grammar.ml
+1 -1 metaprl-branches/opname_classes/filter/phobos/phobos_parser.mly
+28 -26 metaprl-branches/opname_classes/library/basic.ml
+52 -49 metaprl-branches/opname_classes/library/db.ml
+17 -15 metaprl-branches/opname_classes/library/definition.ml
+9 -7 metaprl-branches/opname_classes/library/library.ml
+5 -3 metaprl-branches/opname_classes/library/link.ml
+6 -4 metaprl-branches/opname_classes/library/mbterm.ml
+58 -36 metaprl-branches/opname_classes/library/nuprl5.ml
+40 -38 metaprl-branches/opname_classes/library/orb.ml
+14 -0 metaprl-branches/opname_classes/refiner/refbase/opname.ml
+9 -1 metaprl-branches/opname_classes/refiner/refbase/opname.mli
+14 -6 metaprl-branches/opname_classes/refiner/reflib/ascii_io.ml
+1 -1 metaprl-branches/opname_classes/refiner/reflib/simple_print.ml
+124 -124 metaprl-branches/opname_classes/refiner/reflib/term_order.ml
+4 -4 metaprl-branches/opname_classes/refiner/refsig/term_op_sig.ml
+3 -0 metaprl-branches/opname_classes/refiner/refsig/term_shape_sig.ml
+2 -2 metaprl-branches/opname_classes/refiner/refsig/term_sig.ml
+1 -1 metaprl-branches/opname_classes/refiner/rewrite/rewrite_build_contractum.ml
+4 -2 metaprl-branches/opname_classes/refiner/rewrite/rewrite_debug.ml
+4 -3 metaprl-branches/opname_classes/refiner/rewrite/rewrite_match_redex.ml
+5 -3 metaprl-branches/opname_classes/refiner/rewrite/rewrite_meta.ml
+2 -1 metaprl-branches/opname_classes/refiner/rewrite/rewrite_types.ml
+1 -1 metaprl-branches/opname_classes/refiner/term_ds/term_ds.ml
+1 -1 metaprl-branches/opname_classes/refiner/term_ds/term_ds_sig.ml
+26 -0 metaprl-branches/opname_classes/refiner/term_gen/term_shape_gen.ml
+1 -1 metaprl-branches/opname_classes/refiner/term_std/term_std.ml
+1 -1 metaprl-branches/opname_classes/refiner/term_std/term_std_sig.ml
+5 -1 metaprl-branches/opname_classes/support/shell/shell_core.ml
+5 -1 metaprl-branches/opname_classes/support/shell/shell_package.ml