Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-11 05:10:57 -0800 (Fri, 11 Nov 2005)
Revision: 8163
Log message:
Trying to make "AutoComplete" handling more efficient. In "AutoComplete" mode
we want to abort on first goal that we can not complete, and not go all the
way on all the branches and only then check whether all of them are complete.
Changes | Path |
+8 -3 | metaprl/support/tactics/auto_tactic.ml |