Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-18 19:29:12 -0700 (Fri, 18 Jul 2003)
Revision: 4761
Log message:

      Added sequents to <:con< ... >> quotation.
      Here's a short summary of syntax:
      
         e ::= sequent [args] { hyps >- con_term list }
         args ::= con_term list  -- The usual syntax for these terms
         hyp ::= <H> | <H[con_terms]>
             |   <$e$>           -- $e$ should be a list of hypothesis terms
             |   v:con_term
             |   $v$:con_term
      
      This is the first pass, undoubtly we'll need some tuning.
      

Changes  Path
+6 -0 metaprl/filter/base/filter_type.ml
+30 -1 metaprl/filter/filter/filter_parse.ml
+62 -6 metaprl/filter/filter/term_grammar.ml
+1 -1 metaprl/refiner/refsig/term_sig.ml
+1 -3 mpcompiler/mmc/core/mmc_core_type_infer.ml