Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-14 08:20:34 -0800 (Sat, 14 Jan 2006)
Revision: 8475
Log message:

      I think we do not need the type BSequent for the bterms that represent
      sequents, so I'm going to try and weaken it to BTerm{0}.
      

Changes  Path
+4 -4 metaprl/theories/itt/reflection/experimental/OMakefile
+3 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent.ml
+2856 -2757 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent.prla
+8 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_bterm.ml
+5175 -4366 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_bterm.prla
+7 -7 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_proof1.ml
+8283 -7149 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_proof1.prla
+15 -16 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term1.ml