diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:39:19 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:39:19 +0000 |
| commit | 4de4542daec717b64662150e52a57f808f159972 (patch) | |
| tree | 601ff833f24acce9b451da8c5773fd6abe69809d /tactics/tacticals.mli | |
| parent | 470cc2d01e6c4c2bc0ed109e20e1645c785dccf6 (diff) | |
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
Diffstat (limited to 'tactics/tacticals.mli')
| -rw-r--r-- | tactics/tacticals.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 722cb8b13..efeb4a747 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -185,6 +185,7 @@ module New : sig val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic val tclOR : unit tactic -> unit tactic -> unit tactic val tclONCE : unit tactic -> unit tactic + val tclEXACTLY_ONCE : unit tactic -> unit tactic val tclORELSE0 : unit tactic -> unit tactic -> unit tactic val tclORELSE : unit tactic -> unit tactic -> unit tactic |