Remove some dead code in tacinterp.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17087 85f007b7-540e-0410-9357-904b9bb8a0f7
Update comments in matching.mli.

The comments were inaccurate after r16533.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17088 85f007b7-540e-0410-9357-904b9bb8a0f7
Implementation of Ltac's match and match goal fully based on IStream.

The implementation was partly based on IStream and partly on a control flow with exception. The latter does not mix well with the monadic tactics.

I've moved the algorithmic part of pattern-matching to a new file (tactics/tacticMatching.ml), in order to de-entangle the pattern-matching procedure from the interpretation. This shaves off 300 lines of code from Tacinterp, which is still over 2000 lines of code. It is a first step towards refactoring tacinterp. To be fair, part of what disapeared are lines which sent messages to the debugger. I was not too concerned with them because I understand people found the debugger much too fine-grain on Ltac's pattern matching. But conversely, there may be too few debugging hooks now. This is worth looking into.

In TacticMatching itself, I used a monadic style to express the pattern-matching procedure concisely. I implemented the monad in a fairly brute-force way, using the existing primitive of IStream. It may be worth experimenting with specialized primitive. I am less worried about the monadic style than about the number of allocation of list cells that the primitives entail.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17089 85f007b7-540e-0410-9357-904b9bb8a0f7
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