Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-04 16:12:47 -0700 (Fri, 04 Jun 2004)
Revision: 5855
Log message:

      (Merging the quote_param branch)
      This commit is a first step towards adding reflective reasoning capabilities
      to MetaPRL. This adds:
      - a "Quote" parameter (represented as "@" on I/O)
      - support for basic quoting/unquoting (no variable or sequent support yet) to
        the term modules.
      

Changes  Path
+8 -2 metaprl/filter/base/filter_cache_fun.ml
+5 -3 metaprl/filter/base/filter_magic.ml
+1 -0 metaprl/filter/filter/filter_parse.ml
+2 -0 metaprl/filter/filter/filter_patt.ml
+4 -0 metaprl/filter/filter/term_grammar.ml
+2 -0 metaprl/library/mbterm.ml
+3 -0 metaprl/refiner/reflib/ascii_io.ml
+3 -2 metaprl/refiner/reflib/ascii_io_sig.ml
+1 -0 metaprl/refiner/reflib/simple_print.ml
+1 -0 metaprl/refiner/reflib/term_compare.ml
+2 -0 metaprl/refiner/reflib/term_order.ml
+4 -0 metaprl/refiner/refsig/term_op_sig.ml
+1 -0 metaprl/refiner/refsig/term_shape_sig.ml
+1 -0 metaprl/refiner/refsig/term_sig.ml
+2 -0 metaprl/refiner/rewrite/rewrite.ml
+2 -0 metaprl/refiner/rewrite/rewrite_build_contractum.ml
+2 -1 metaprl/refiner/rewrite/rewrite_compile_contractum.ml
+1 -0 metaprl/refiner/rewrite/rewrite_compile_redex.ml
+4 -0 metaprl/refiner/rewrite/rewrite_debug.ml
+1 -0 metaprl/refiner/rewrite/rewrite_match_redex.ml
+3 -0 metaprl/refiner/rewrite/rewrite_meta.ml
+1 -0 metaprl/refiner/rewrite/rewrite_types.ml
+1 -0 metaprl/refiner/term_ds/term_man_ds.ml
+26 -0 metaprl/refiner/term_ds/term_op_ds.ml
+1 -1 metaprl/refiner/term_gen/term_header_constr.ml
+1 -0 metaprl/refiner/term_gen/term_man_gen.ml
+5 -0 metaprl/refiner/term_gen/term_shape_gen.ml
+13 -0 metaprl/refiner/term_std/term_op_std.ml