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 |