Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-28 21:06:59 -0800 (Wed, 28 Jan 2004)
Revision: 5309
Log message:

      No longer need to put (or allowed to put) the last sequent context into
      the list of rule/rewrite arguments, even when there are non-context hypotheses
      after that.
      

Changes  Path
+8 -8 metaprl/editor/ml/tests/prop-pigeon.ml
+1 -1 metaprl/editor/ml/tests/test.ml
+19 -13 metaprl/refiner/refiner/refine.ml
+15 -8 metaprl/refiner/rewrite/rewrite_compile_redex.ml
+1 -1 metaprl/refiner/rewrite/rewrite_match_redex.ml
+3 -0 metaprl/refiner/rewrite/rewrite_types.ml
+9 -9 metaprl/theories/czf/czf_itt_bool.ml
+2 -2 metaprl/theories/itt/ctt_markov.ml
+1 -1 metaprl/theories/itt/itt_antiquotient.ml
+2 -2 metaprl/theories/itt/itt_antiquotient.prla
+2 -2 metaprl/theories/itt/itt_eq_base.prla
+6 -6 metaprl/theories/itt/itt_int_arith.ml
+10 -10 metaprl/theories/itt/itt_relation_str.ml
+20 -43 metaprl/theories/itt/itt_subset.ml
+2 -2 metaprl/theories/itt/itt_supinf.ml
+1 -1 metaprl/theories/itt/itt_test.ml
+1 -1 metaprl/theories/itt/jprover_tests.ml