From f88eba17b779c1a38e2ad332f9e4cc6bd04f57d6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Apr 2001 02:53:00 +0000
Subject: Bug affichage LETPATTERN

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

(limited to 'syntax')

diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v
index 5074dfd890..bdedb15c61 100644
--- a/syntax/PPTactic.v
+++ b/syntax/PPTactic.v
@@ -192,8 +192,10 @@ Syntax tactic
   | absurd [<<(Absurd $C)>>] -> ["Absurd " $C]
 
   | cut [<<(Cut $C)>>] -> ["Cut " $C]
-  | lettac [<<(LetTac $id $c (LETPATTERNS ($LIST $pl)))>>] -> 
-	["LetTac" [1 1] $id ":=" $c [1 1] "in" [1 1] (LETPATTERNS ($LIST $pl))]
+  | lettac_cons [<<(LetTac $id $c (LETPATTERNS $p ($LIST $pl)))>>] -> 
+	["LetTac" [1 1] $id ":=" $c [1 1] "in" [1 1] (LETPATTERNS $p ($LIST $pl))]
+  | lettac_nil [<<(LetTac $id $c (LETPATTERNS))>>] -> 
+	["LetTac" [1 1] $id ":=" $c]
 
   | left [<<(Left $b)>>] -> ["Left" (WITHBINDING $b)]
   | right [<<(Right $b)>>] -> [ "Right" (WITHBINDING $b)]
-- 
cgit v1.2.3