From ded597434229e373243f8d320ce51aaa4e35981f Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 16 Oct 2003 18:32:23 +0000
Subject: lettac -> set suppression de la notation carre de R

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4659 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 translate/ppconstrnew.ml | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

(limited to 'translate/ppconstrnew.ml')

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 281ca2c5c6..7e71f56239 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -394,12 +394,14 @@ let rec pr inherited a =
   | CRef r -> pr_reference r, latom
   | CFix (_,id,fix) ->
       let p = hov 0 (str"fix " ++ pr_recursive (pr_fixdecl pr) (snd id) fix) in
-      (if List.length fix = 1 & prec_less (fst inherited) ltop
-       then surround p else p),
-      lfix
+      if List.length fix = 1 & prec_less (fst inherited) ltop
+      then surround p, latom else p, lfix
   | CCoFix (_,id,cofix) ->
-      hov 0 (str "cofix " ++ pr_recursive (pr_cofixdecl pr) (snd id) cofix),
-      lfix
+      let p =
+        hov 0 (str "cofix " ++
+               pr_recursive (pr_cofixdecl pr) (snd id) cofix) in
+      if List.length cofix = 1 & prec_less (fst inherited) ltop
+      then surround p, latom else p, lfix
   | CArrow (_,a,b) ->
       hov 0 (pr (larrow,L) a ++ str " ->" ++ brk(1,0) ++ pr (-larrow,E) b),
       larrow
@@ -504,9 +506,6 @@ let rec pr inherited a =
         str "end"),
       latom
   | CHole _ -> str "_", latom
-(*
-  | CEvar (_,n) -> str "?" ++ int n, latom
-*)
   | CEvar (_,n) -> str (Evd.string_of_existential n), latom
   | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
   | CSort (_,s) -> pr_sort s, latom
-- 
cgit v1.2.3