Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-01 09:15:20 -0800 (Sun, 01 Jan 2006)
Revision: 8387
Log message:

      Rephrased the Provable intro rules, using the SubLogic judgment
      instead of a fixed logic.
      

Changes  Path
+154 -94 metaprl/filter/base/filter_reflection.ml
+4 -10 metaprl/filter/base/filter_reflection.mli
+1 -1 metaprl/filter/base/filter_type.ml
+42 -93 metaprl/filter/filter/filter_parse.ml
+3 -5 metaprl/filter/filter/term_grammar.ml
+4 -1 metaprl/refiner/refiner/refiner_debug.ml
+1 -0 metaprl/refiner/refsig/term_man_sig.ml
+1 -0 metaprl/refiner/term_ds/term_man_ds.ml
+3 -0 metaprl/refiner/term_gen/term_man_gen.ml
+0 -1 metaprl/support/display/perv.mli
+5 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_meta_types.ml
+17 -6 metaprl/theories/itt/reflection/experimental/itt_hoas_proof.ml
+5 -1 metaprl/theories/itt/reflection/experimental/itt_hoas_proof.mli
+328 -357 metaprl/theories/itt/reflection/experimental/itt_hoas_proof.prla
+0 -35 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term.ml
+0 -9 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term.mli
+0 -8 metaprl/theories/meta/base/base_grammar.mli
+1 -1 metaprl/theories/poplmark/naive/pmn_core_terms.ml