Changes the semantics of Ltac's non-lazy pattern matching in presence of multiple successes.

The semantics was a bit strange: an immediate failure of a branch would cause the pattern matching to backtrack, and failure after the match could cause the selected tactic to backtrack. However, the pattern matching process won't backtrack after it has selected a tactic with at least one success.

To avoid changing the semantics of pattern matching with single-success tactics, I made it so that it is impossible to backtrack into a pattern matching once done.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17090 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions