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