From af63420fe7202f01b483812bc1f5ff50c5a640e2 Mon Sep 17 00:00:00 2001
From: aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 2 Nov 2013 15:38:41 +0000
Subject: 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
---
 tactics/tacinterp.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'tactics/tacinterp.ml')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2bf3c8e06..34ea3dc87 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)
-- 
cgit v1.2.3