From fafd9c0fbc366185fe3bf9697524687a65e0b7c2 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:38:16 +0000
Subject: Added the tactical "tac1 + tac2".

It works pretty much like "tac1 || tac2" except that it has as successes all the successes of tac1 followed by all the successes of tac2 (whereas the latter has either the successes of tac1 (if there is at least one) or those of tac2 (otherwise)).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16998 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 printing/pptactic.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'printing/pptactic.ml')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index a771184716..61f758df01 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -886,6 +886,11 @@ let rec pr_tac inherited tac =
   | TacInfo t ->
       hov 1 (str "info" ++ spc () ++ pr_tac (ltactical,E) t),
       linfo
+  | TacOr (t1,t2) ->
+      (* arnaud: vérifier qu'il s'agit bien de la syntaxe définitive. *)
+      hov 1 (pr_tac (lorelse,L) t1 ++ str " +" ++ brk (1,1) ++
+             pr_tac (lorelse,E) t2),
+      lorelse
   | TacOrelse (t1,t2) ->
       hov 1 (pr_tac (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++
              pr_tac (lorelse,E) t2),
-- 
cgit v1.2.3