Adds an experimental exactly_once tactical.

exactly_once t, will have a success if t has exactly once success.

There are a few caveats:
- The underlying effects of t may happen in an unpredictable order (hence it may be wise to use it only with "pure" tactics)
- The second success of a tactic is conditional on the exception thrown. In Ltac it doesn't show, but in the underlying code, the tactical also expects the exception you want to use to produce the second success.

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

0 files changed, 0 insertions, 0 deletions