Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-18 13:11:12 -0800 (Sat, 18 Mar 2006)
Revision: 8935
Log message:

      
      Added theory inheritance.
      
      This also changes the elimination rules to include the
      sub-logics.
      

Changes  Path
+9 -7 metaprl/filter/base/filter_reflection.ml
+3 -3 metaprl/filter/base/filter_reflection.mli
+7 -5 metaprl/filter/filter/filter_bin.ml
+50 -22 metaprl/filter/filter/filter_reflect.ml
+1 -1 metaprl/filter/filter/filter_reflect.mli
+1 -0 metaprl/theories/itt/reflection/MetaprlInfo
Properties metaprl/theories/itt/reflection/base
Copied metaprl/theories/itt/reflection/base/MetaprlInfo
+14 -0 metaprl/theories/itt/reflection/base/MetaprlInfo
Added metaprl/theories/itt/reflection/base/itt_hoas_base_theory.ml
Properties metaprl/theories/itt/reflection/base/itt_hoas_base_theory.ml
Added metaprl/theories/itt/reflection/base/itt_hoas_base_theory.mli
Properties metaprl/theories/itt/reflection/base/itt_hoas_base_theory.mli
Added metaprl/theories/itt/reflection/base/reflect_base_theory.ml
Properties metaprl/theories/itt/reflection/base/reflect_base_theory.ml
Added metaprl/theories/itt/reflection/base/reflect_base_theory.mli
Properties metaprl/theories/itt/reflection/base/reflect_base_theory.mli
Added metaprl/theories/itt/reflection/base/reflect_base_theory.prla
Properties metaprl/theories/itt/reflection/base/reflect_base_theory.prla
+0 -0 metaprl/theories/itt/reflection/experimental/MetaprlInfo
+0 -2 metaprl/theories/meta/base/MetaprlInfo
Deleted metaprl/theories/meta/base/reflect_base_theory.mlz
+1 -0 metaprl/theories/poplmark/naive/MetaprlInfo
+4 -0 metaprl/theories/poplmark/naive/pmn_core_judgments.mli
+0 -2 metaprl/theories/poplmark/naive/pmn_core_logic.ml
+0 -4 metaprl/theories/poplmark/naive/pmn_core_logic.mli
+38 -36 metaprl/util/ocamldep.mll