From 8640627fa00798b429baf56937a66f1621be0a02 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 8 Nov 2001 14:05:24 +0000
Subject: Prise en compte de la syntaxe [x:=c:t]b comme équivalent de
 [x:=c::t]b

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

(limited to 'syntax')

diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v
index f78ef411ea..ee259cbfa1 100755
--- a/syntax/PPConstr.v
+++ b/syntax/PPConstr.v
@@ -144,8 +144,11 @@ Syntax constr
 	 [ $A:L [0 0] "->" (ARROWBOX $B) ]
 
 (* These are synonymous *)
+(* redundant
   | let [ [$x = $M]$N ] -> [ [<hov 0> "[" $x "=" $M:E "]" [0 1] $N:E ] ]
+*)
   | letin [ [$x := $A]$B ] -> [ [ <hov 0> "[" $x ":=" $A:E "]" [0 1] $B:E ] ]
+  | letincast [ [$x := $A : $C]$B ] -> [ [ <hov 0> "[" $x ":=" $A:E ":" $C:E "]" [0 1] $B:E ] ]
   ;
 
 (* Things parsed in command9 *)
-- 
cgit v1.2.3