Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-29 20:22:54 -0700 (Fri, 29 Jun 2001)
Revision: 3304
Log message:

      Added num_assums and nth_assums to Refine and Sequent.
      

Changes  Path
+2 -0 metaprl/filter/boot/sequent_boot.ml
+4 -0 metaprl/filter/boot/tactic_boot.ml
+4 -0 metaprl/filter/boot/tactic_boot_sig.mlz
+7 -10 metaprl/filter/boot/tacticals_boot.ml
+2 -0 metaprl/refiner/refiner/refine.ml
+2 -0 metaprl/refiner/refsig/refine_sig.ml
+3 -4 metaprl/theories/itt/itt_collection.ml
+9 -10 metaprl/theories/itt/itt_logic.ml
+2 -3 metaprl/theories/itt/itt_struct.ml