diff options
| author | aspiwack | 2013-11-02 15:39:19 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-02 15:39:19 +0000 |
| commit | 4de4542daec717b64662150e52a57f808f159972 (patch) | |
| tree | 601ff833f24acce9b451da8c5773fd6abe69809d /tactics | |
| 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')
| -rw-r--r-- | tactics/tacintern.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 1 |
5 files changed, 9 insertions, 0 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 2f41ff2aea..42ea649ecd 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -691,6 +691,8 @@ and intern_tactic_seq onlytac ist = function ist.ltacvars, TacOr (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2) | TacOnce tac -> ist.ltacvars, TacOnce (intern_pure_tactic ist tac) + | TacExactlyOnce tac -> + ist.ltacvars, TacExactlyOnce (intern_pure_tactic ist tac) | TacOrelse (tac1,tac2) -> ist.ltacvars, TacOrelse (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2) | TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_pure_tactic ist) l) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 2c64b669c5..edb9ab66d3 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1141,6 +1141,8 @@ and eval_tactic ist = function Tacticals.New.tclOR (interp_tactic ist tac1) (interp_tactic ist tac2) | TacOnce tac -> Tacticals.New.tclONCE (interp_tactic ist tac) + | TacExactlyOnce tac -> + Tacticals.New.tclEXACTLY_ONCE (interp_tactic ist tac) | TacOrelse (tac1,tac2) -> Tacticals.New.tclORELSE (interp_tactic ist tac1) (interp_tactic ist tac2) | TacFirst l -> Tacticals.New.tclFIRST (List.map (interp_tactic ist) l) diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 44327abef2..7c968865ac 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -251,6 +251,8 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with TacOr (subst_tactic subst tac1,subst_tactic subst tac2) | TacOnce tac -> TacOnce (subst_tactic subst tac) + | TacExactlyOnce tac -> + TacExactlyOnce (subst_tactic subst tac) | TacOrelse (tac1,tac2) -> TacOrelse (subst_tactic subst tac1,subst_tactic subst tac2) | TacFirst l -> TacFirst (List.map (subst_tactic subst) l) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 1b8cf531bc..f25bae9bb8 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -400,6 +400,8 @@ module New = struct let tclONCE = Proofview.tclONCE + let tclEXACTLY_ONCE t = Proofview.tclEXACTLY_ONCE (Refiner.FailError(0,lazy (assert false))) t + let tclORELSE0 t1 t2 = tclINDEPENDENT begin tclORELSE diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 722cb8b135..efeb4a7478 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 |