diff options
| author | barras | 2003-10-16 18:32:23 +0000 |
|---|---|---|
| committer | barras | 2003-10-16 18:32:23 +0000 |
| commit | ded597434229e373243f8d320ce51aaa4e35981f (patch) | |
| tree | f3ff61a8ac2fa445a642eaf574d2b562126dcd1f /translate/ppconstrnew.ml | |
| parent | a69a28443fad9374d6ac9f3fe02d0270577fdba6 (diff) | |
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
Diffstat (limited to 'translate/ppconstrnew.ml')
| -rw-r--r-- | translate/ppconstrnew.ml | 15 |
1 files changed, 7 insertions, 8 deletions
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 |