diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:39:19 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:39:19 +0000 |
| commit | 4de4542daec717b64662150e52a57f808f159972 (patch) | |
| tree | 601ff833f24acce9b451da8c5773fd6abe69809d /printing | |
| 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 'printing')
| -rw-r--r-- | printing/pptactic.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index f0d713be4..c5a8a380d 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -895,6 +895,10 @@ let rec pr_tac inherited tac = (* arnaud: vérifier qu'il s'agit bien de la syntaxe définitive. *) hov 1 (str "once" ++ spc () ++ pr_tac (ltactical,E) t), ltactical + | TacExactlyOnce t -> + (* arnaud: vérifier qu'il s'agit bien de la syntaxe définitive. *) + hov 1 (str "exactly_once" ++ spc () ++ pr_tac (ltactical,E) t), + ltactical | TacOrelse (t1,t2) -> hov 1 (pr_tac (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++ pr_tac (lorelse,E) t2), |