Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-04 01:12:47 -0800 (Sat, 04 Dec 2004)
Revision: 6330
Log message:

      - Fixed a few minor bugs in handling of non-sequent contexts.
      
      - Added an input syntax for non-sequent context terms
        ( 'V<|C;...;C|>[[t]][t;...;t], where "<|...|>" and "[...]" are optional)
      
      Note that this is only a small part of what will be needed to fully support
      non-sequent contexts. The rewriter and filter code for non-sequent contexts is
      still incomplete (the biggest problem is that we currently only allow term and
      int paramaters in primitive rules, while non-sequent contexts require address
      parameters) and would not work.
      

Changes  Path
+6 -0 metaprl/filter/filter/term_grammar.ml
+4 -4 metaprl/refiner/rewrite/rewrite_compile_contractum.ml
+5 -1 metaprl/refiner/term_ds/term_subst_ds.ml
+4 -0 metaprl/refiner/term_gen/term_meta_gen.ml
+4 -0 metaprl/theories/itt/itt_test.ml