From 7ce9a2c43420d694a901c152d95b6645c76d34cd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 27 Apr 2003 18:32:34 +0000
Subject: Affichage des Fix contenant des Let dans leur context (ce que la
 tactique Fix permet)

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

(limited to 'syntax')

diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v
index 0b111a69f1..492c5cbbaa 100755
--- a/syntax/PPConstr.v
+++ b/syntax/PPConstr.v
@@ -33,7 +33,9 @@ Syntax constr
   | bindersone  [ << (BINDERS (BINDER $c ($LIST $id))) >> ] -> 
        [ [<hov 0> (IDBINDER ($LIST $id))] ":" $c:E ]
 
-  | letbinder  [ << (BINDERS (LETBINDER $c $id)) >> ] -> 
+  | letbindercons [ << (BINDERS (LETBINDER $c $id) ($LIST $b)) >> ] ->
+       [ [<hov 0> id ":=" [0 1] $c:E ";" [1 0] (BINDERS ($LIST $b)) ] ]
+  | letbinderone  [ << (BINDERS (LETBINDER $c $id)) >> ] -> 
        [ [<hov 0> id ":=" [0 1] $c:E ] ]
   ;
 
-- 
cgit v1.2.3