Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-19 23:02:32 -0800 (Thu, 19 Feb 2004)
Revision: 5389
Log message:

      itt_int_arith: added "cacheT info tac" which runs tac once,
      memorizes all aux-goals, assert them, reruns tac and complete
      all aux-goals with nthHypT.
      
      tactic_boot_sig: exposed type extract and function refine in TacticSig in order
      to be able to rerun a tactic. This might go away if we decide to move cacheT
      to the "general purpose library".
      

Changes	Path
+5 -0	metaprl/tactics/proof/tactic_boot_sig.ml
+86 -6	metaprl/theories/itt/itt_int_arith.ml