Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-24 15:08:04 -0800 (Tue, 24 Jan 2006)
Revision: 8598
Log message:

      Try to be more careful about using length{vlist{| <J> |}} as
      the canonical expression for the length of a context.
      
      Temporarily remove poplmark/naive from THEORIES_ALL until
      the proofs terminate.
      

Changes  Path
+113 -109 metaprl/filter/base/filter_reflection.ml
+1 -1 metaprl/mk/defaults
+16 -27 metaprl/theories/itt/reflection/experimental/itt_hoas_relax.ml
+6211 -6358 metaprl/theories/itt/reflection/experimental/itt_hoas_relax.prla
+1 -0 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_proof.ml
+16 -30 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term.ml
+1 -1 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term.mli
+3236 -3470 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term.prla