Do not print tactic notation names at each interpretation step.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17082 85f007b7-540e-0410-9357-904b9bb8a0f7
Useless computation in Goal handle augmentation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17083 85f007b7-540e-0410-9357-904b9bb8a0f7
Synchronizing the printer of tactic notations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17084 85f007b7-540e-0410-9357-904b9bb8a0f7
Adding an unsafe mapping function to maps.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17085 85f007b7-540e-0410-9357-904b9bb8a0f7
Fast lookup_named in environments, based on maps instead of lists.
This was quite a severe performance bottleneck.

Ideally, this data structure should be put into contexts, but the relevant
type is transparent... For now, we stick to this inelegant workaround.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17086 85f007b7-540e-0410-9357-904b9bb8a0f7
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
Revert "Fast lookup_named in environments, based on maps instead of lists."

Contrarily to my machine results, it seems that it tore down the performance of
Coq on benchmarks.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17091 85f007b7-540e-0410-9357-904b9bb8a0f7
bugfix micromega: solved an ambiguous symbol resolution

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17093 85f007b7-540e-0410-9357-904b9bb8a0f7
Slightly faster version of merging substitutions in TacticMatching.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17094 85f007b7-540e-0410-9357-904b9bb8a0f7
Adding generic solvers to term holes. For now, no resolution mechanism nor
parsing is plugged.
Adding the necessary hooks to handle tactics in terms.
Actually adding the grammar entry to handle tactics in terms.