diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:41:49 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:41:49 +0000 |
| commit | 4ac1b34ff8afc250e34d0b229c0a3608ed83e640 (patch) | |
| tree | c7c7ed74f7f4f1d68e067dade31042b7620e986a /printing | |
| parent | 0b936be00d2c7c05d528b8d7304fc1e14d5546a5 (diff) | |
Update comments.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17033 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'printing')
| -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) -> |