From 265365329632320e3880e792712c8223c1cb1316 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 3 Oct 2000 18:12:46 +0000
Subject: Ajout castedopenconstrarg; Renommage tactique Let en LetTac

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@640 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_tactic.ml4 | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index d0e3a8a76f..eb4bc02e4b 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -30,6 +30,9 @@ GEXTEND Gram
   constrarg:
     [ [ c = Constr.constr -> <:ast< (COMMAND $c) >> ] ]
   ;
+  castedopenconstrarg:
+    [ [ c = Constr.constr -> <:ast< (CASTEDOPENCOMMAND $c) >> ] ]
+  ;
   lconstrarg:
     [ [ c = Constr.lconstr -> <:ast< (COMMAND $c) >> ] ]
   ;
@@ -369,7 +372,7 @@ GEXTEND Gram
           <:ast< (Generalize ($LIST $lc)) >>
       | IDENT "Generalize"; IDENT "Dependent"; c = constrarg ->
           <:ast< (GeneralizeDep $c) >>
-      | IDENT "Let"; s = identarg; ":="; c = constrarg; "in";
+      | IDENT "LetTac"; s = identarg; ":="; c = constrarg; "in";
 	  l = ne_pattern_hyp_list -> 
 	    <:ast< (LetTac $s $c (LETPATTERNS ($LIST $l))) >>
       | IDENT "LApply"; c = constrarg -> <:ast< (CutAndApply $c) >>
-- 
cgit v1.2.3