aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2004-02-20 14:34:21 +0000
committerherbelin2004-02-20 14:34:21 +0000
commit36a6da6a1256f489b63170f8102bc904ba340c2b (patch)
treea769001acc98b969ec0d26d0ca5a616ab011cb07
parent0dba924aad1566c914106899e9e1a6d245e08628 (diff)
commit précédent erroné
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5366 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--translate/ppconstrnew.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index f8d81c2430..9b2faf4ba9 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -537,7 +537,6 @@ let rec pr sep inherited a =
hov 0 (str "else" ++ pr (fun () -> brk (1,1)) ltop b2)),
lif
-(*
| COrderedCase (_,st,po,c,[b1;b2]) when st = IfStyle ->
(* On force les parenthèses autour d'un "if" sous-terme (même si le
parsing est lui plus tolérant) *)
@@ -557,7 +556,7 @@ let rec pr sep inherited a =
pr spc ltop c ++ str " in") ++
pr spc ltop b),
lletin
-*)
+
| COrderedCase (_,style,po,c,bl) ->
hv 0 (
str (if style=MatchStyle then "old_match " else "match ") ++