Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-21 02:41:52 -0800 (Tue, 21 Jan 2003)
Revision: 4001
Log message:

      For ThinOption in elim resource, determine the hyp number for thinning
      upfront (when processing the annotation) instead of trying to guess it at
      run-time based on the hyp. variable names.
      

Changes  Path
+33 -17 metaprl/theories/base/base_dtactic.ml
+3 -3 metaprl/theories/itt/itt_bool.ml