diff options
| author | aspiwack | 2013-11-02 15:38:41 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-02 15:38:41 +0000 |
| commit | af63420fe7202f01b483812bc1f5ff50c5a640e2 (patch) | |
| tree | eb124c5a451cb55a3080093994b14a8960251a68 /tactics | |
| parent | a9cfc4691726ac248dc7bbc43bb5ae8a7db3233f (diff) | |
Adds a tactical once.
[once t] does just as [t] but has exactly one success it [t] has at least one success.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17004 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 ddabb5d089..2f41ff2aea 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -689,6 +689,8 @@ and intern_tactic_seq onlytac ist = function ist.ltacvars, TacTimeout (intern_or_var ist n,intern_tactic onlytac ist tac) | TacOr (tac1,tac2) -> ist.ltacvars, TacOr (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2) + | TacOnce tac -> + ist.ltacvars, TacOnce (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 2bf3c8e065..34ea3dc877 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1139,6 +1139,8 @@ and eval_tactic ist = function | TacRepeat tac -> Tacticals.New.tclREPEAT (interp_tactic ist tac) | TacOr (tac1,tac2) -> Tacticals.New.tclOR (interp_tactic ist tac1) (interp_tactic ist tac2) + | TacOnce tac -> + Tacticals.New.tclONCE (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 ba37c10191..44327abef2 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -249,6 +249,8 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with | TacRepeat tac -> TacRepeat (subst_tactic subst tac) | TacOr (tac1,tac2) -> TacOr (subst_tactic subst tac1,subst_tactic subst tac2) + | TacOnce tac -> + TacOnce (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 574e4c9a92..2131dc4807 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -398,6 +398,8 @@ module New = struct end end + let tclONCE = Proofview.tclONCE + let tclORELSE0 t1 t2 = tclINDEPENDENT begin tclORELSE diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index f7ba178a31..722cb8b135 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -184,6 +184,7 @@ module New : sig THIS MODULE. *) val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic val tclOR : unit tactic -> unit tactic -> unit tactic + val tclONCE : unit tactic -> unit tactic val tclORELSE0 : unit tactic -> unit tactic -> unit tactic val tclORELSE : unit tactic -> unit tactic -> unit tactic |