From 8e13e6233ee4fc002f42290f1b7ae64a6e627162 Mon Sep 17 00:00:00 2001
From: gregoire
Date: Wed, 26 Mar 2003 14:02:21 +0000
Subject: Ajout de Set Print Width

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3790 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 syntax/PPConstr.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'syntax')

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 *)
-- 
cgit v1.2.3