Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-27 08:59:07 -0800 (Mon, 27 Mar 2006)
Revision: 8955
Log message:

      Proved a bunch of theorems about well-formedness of
      reflected terms.  This solves most of the intro proofs
      for elimination-style rules.  I'll finish it off soon.
      
      There were a couple of conflicts with .prla files.
      I've renamed my copies to .prla2.  I'll see what I can
      do to merge them.
      

Changes  Path
+2 -0 metaprl/theories/itt/core/itt_list2.mli
+42 -0 metaprl/theories/itt/core/itt_struct2.ml
+1 -0 metaprl/theories/itt/core/itt_struct2.mli
+59 -1 metaprl/theories/itt/extensions/vector/itt_vec_bind.ml
+3419 -3358 metaprl/theories/itt/extensions/vector/itt_vec_bind.prla
+2 -0 metaprl/theories/itt/extensions/vector/itt_vec_list1.mli
+3549 -3799 metaprl/theories/itt/extensions/vector/itt_vec_sequent_term.prla
+16 -0 metaprl/theories/itt/reflection/core/itt_hoas_debruijn.ml
+1092 -513 metaprl/theories/itt/reflection/core/itt_hoas_debruijn.prla
+4 -0 metaprl/theories/itt/reflection/core/itt_hoas_vbind.ml
+1 -0 metaprl/theories/itt/reflection/experimental/MetaprlInfo
+27 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_bterm_wf.ml
+3009 -5086 metaprl/theories/itt/reflection/experimental/itt_hoas_bterm_wf.prla
Copied metaprl/theories/itt/reflection/experimental/itt_hoas_bterm_wf.prla2
+16102 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_bterm_wf.prla2
+34 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_lof.ml
+3902 -2350 metaprl/theories/itt/reflection/experimental/itt_hoas_lof.prla
+41 -4 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent.ml
+6951 -6489 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent.prla
Copied metaprl/theories/itt/reflection/experimental/itt_hoas_sequent.prla2
+18812 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent.prla2
+66 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term.ml
+5103 -5047 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term.prla
Added metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term_wf.ml
Added metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term_wf.mli
Added metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term_wf.prla
+1 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_theory.mlz
+1 -1 metaprl/theories/poplmark/naive/pmn_core_logic.ml