From f493b6f2b103dd4e2d0b86acae2fcc7a2b76bdcf Mon Sep 17 00:00:00 2001
From: delahaye
Date: Wed, 7 Feb 2001 16:24:53 +0000
Subject: Modif pour les patterns de sous-termes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1347 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_tactic.ml4 | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 4daad6f5e9..f4b0e01e58 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -231,12 +231,7 @@ GEXTEND Gram
           <:ast< (RECCLAUSE $name (FUNVAR ($LIST $it)) $body) >> ] ]
   ;
   match_pattern:
-    [ [ id = constrarg; "["; pc = constrarg; "]" ->
-          (match id with
-          | Coqast.Node(_,"COMMAND",[Coqast.Nvar(_,s)]) ->
-            <:ast< (SUBTERM ($VAR $s) $pc) >>
-          | _ ->
-            errorlabstrm "Gram.match_pattern" [<'sTR "Not a correct SUBTERM">])
+    [ [ id = identarg; "["; pc = constrarg; "]" -> <:ast< (SUBTERM $id $pc) >>
       | "["; pc = constrarg; "]" -> <:ast< (SUBTERM $pc) >>
       | pc = constrarg -> <:ast< (TERM $pc) >> ] ]
   ;
-- 
cgit v1.2.3