Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-24 19:40:51 -0800 (Tue, 24 Jan 2006)
Revision: 8601
Log message:

      Split the judgments out of Pmn_core_terms.
      
      An initial thought here is to define the meta-type judgment
      manually for sequents, rather than use the existential types.
      
      According to our plan, we don't plan to have wf judgments
      for sequents.  However, we see that Filter_{parse,reflection}
      are doing the wrong thing on actual rules (as opposed to
      declare statements), so I'll fix that.
      

Changes  Path
Properties metaprl
+1 -0 metaprl/theories/poplmark/naive/MetaprlInfo
Added metaprl/theories/poplmark/naive/pmn_core_judgments.ml
Properties metaprl/theories/poplmark/naive/pmn_core_judgments.ml
Added metaprl/theories/poplmark/naive/pmn_core_judgments.mli
Properties metaprl/theories/poplmark/naive/pmn_core_judgments.mli
+31 -78 metaprl/theories/poplmark/naive/pmn_core_terms.ml
+0 -114 metaprl/theories/poplmark/naive/pmn_core_terms.mli