From af63420fe7202f01b483812bc1f5ff50c5a640e2 Mon Sep 17 00:00:00 2001
From: aspiwack
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
---
 intf/tacexpr.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index fece993120..839294c0a1 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -217,6 +217,8 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr =
   | TacOr of
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr *
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
+  | TacOnce of
+      ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacOrelse of
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr *
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
-- 
cgit v1.2.3