Ajout de Set Print Width

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3790 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 3 deletions

diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v
index ddc6e35638..9094b0395c 100755
--- a/syntax/PPConstr.v
+++ b/syntax/PPConstr.v
@@ -34,7 +34,7 @@ Syntax constr
        [ [<hov 0> (IDBINDER ($LIST $id))] ":" $c:E ]
 
   | letbinder  [ << (BINDERS (LETBINDER $c $id)) >> ] -> 
-       [ [<hov 0> $id ":=" $c:E ] ]
+       [ [<hov 0> id ":=" [0 1] $c:E ] ]
   ;
 
 
@@ -146,8 +146,8 @@ Syntax constr
 (* redundant
   | let [ [$x = $M]$N ] -> [ [<hov 0> "[" $x "=" $M:E "]" [0 1] $N:E ] ]
 *)
-  | letin [ << (LETIN $A [$x]$B) >> ] -> [ [ <hov 0> "[" $x ":=" $A:E "]" [0 1] $B:E ] ]
-  | letincast [ << (LETIN (CAST $A $C) [$x]$B) >> ] -> [ [ <hov 0> "[" $x ":=" $A:E ":" $C:E "]" [0 1] $B:E ] ]
+  | letin [ << (LETIN $A [$x]$B) >> ] -> [ [ <hov 0> "[" $x ":=" [0 1] $A:E "]" [0 1] $B:E ] ]
+  | letincast [ << (LETIN (CAST $A $C) [$x]$B) >> ] -> [ [ <hov 0> "[" $x ":=" [0 1] $A:E ":" $C:E "]" [0 1] $B:E ] ]
   ;
 
 (* Things parsed in command9 *)