Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-05 15:50:05 -0800 (Sat, 05 Nov 2005)
Revision: 8110
Log message:

      Trying out the "well-formedness"-based Fsub logic.
      

Changes  Path
+11 -0 metaprl/theories/base/base_grammar.mli
+54 -70 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_native.ml
+3 -3 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_native.mli
+1922 -2567 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_native.prla
+2 -3 metaprl/theories/poplmark/naive/OMakefile
Deleted metaprl/theories/poplmark/naive/pmn_core_judgments.ml
Deleted metaprl/theories/poplmark/naive/pmn_core_judgments.mli
Added metaprl/theories/poplmark/naive/pmn_core_logic.ml
Properties metaprl/theories/poplmark/naive/pmn_core_logic.ml
Added metaprl/theories/poplmark/naive/pmn_core_logic.mli
Properties metaprl/theories/poplmark/naive/pmn_core_logic.mli
Deleted metaprl/theories/poplmark/naive/pmn_core_subtype.ml
Deleted metaprl/theories/poplmark/naive/pmn_core_subtype.mli
+7 -215 metaprl/theories/poplmark/naive/pmn_core_terms.ml
+29 -37 metaprl/theories/poplmark/naive/pmn_core_terms.mli