From 4de4542daec717b64662150e52a57f808f159972 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Sat, 2 Nov 2013 15:39:19 +0000 Subject: 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 --- parsing/g_ltac.ml4 | 1 + 1 file changed, 1 insertion(+) (limited to 'parsing/g_ltac.ml4') diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 033de89df..d075a7790 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -67,6 +67,7 @@ GEXTEND Gram | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta | IDENT "progress"; ta = tactic_expr -> TacProgress ta | IDENT "once"; ta = tactic_expr -> TacOnce ta + | IDENT "exactly_once"; ta = tactic_expr -> TacExactlyOnce ta | IDENT "infoH"; ta = tactic_expr -> TacShowHyps ta (*To do: put Abstract in Refiner*) | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None) -- cgit v1.2.3