Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-20 17:00:45 -0800 (Fri, 20 Jan 2006)
Revision: 8542
Log message:

      Made the reduce_sequent_ind_base1 rewrite more conservative.
      

Changes  Path
+0 -4 metaprl/theories/itt/extensions/vector/itt_vec_list1.ml
+15 -66 metaprl/theories/meta/extensions/meta_context_terms.ml
+11 -15 metaprl/theories/meta/extensions/meta_context_terms.mli
+4 -5 metaprl/theories/meta/extensions/meta_context_terms2.ml
+6 -6 metaprl/theories/meta/extensions/meta_context_terms2.mli