diff options
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index c5a8a380d..2ce3eba06 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -887,16 +887,13 @@ let rec pr_tac inherited tac = 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 | TacOnce t -> - (* 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) -> |