From 736e19d7cb974952ac1e7b133476a15f0d2e1147 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 3 Oct 2000 18:14:02 +0000
Subject: Renommage tactique Let en LetTac

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

diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v
index e9a5f11b54..769229af2f 100644
--- a/syntax/PPTactic.v
+++ b/syntax/PPTactic.v
@@ -160,7 +160,7 @@ Syntax tactic
 
   | cut [(Cut $C)] -> ["Cut " $C]
   | lettac [(LetTac $id $c (LETPATTERNS ($LIST $pl)))] -> 
-	["Let" [1 1] $id ":=" $c [1 1] "in" [1 1] (LETPATTERNS ($LIST $pl))]
+	["LetTac" [1 1] $id ":=" $c [1 1] "in" [1 1] (LETPATTERNS ($LIST $pl))]
 
   | left [(Left $b)] -> ["Left" (WITHBINDING $b)]
   | right [(Right $b)] -> [ "Right" (WITHBINDING $b)]
-- 
cgit v1.2.3