From 32e4b999885f34e89077c5a4d686f75b9633ad87 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 23 Nov 2000 13:27:04 +0000
Subject: Bug qualidconstarg (intervient pour Transparent)

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

(limited to 'parsing')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index bcbb32d5b..39bdda79b 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -55,7 +55,7 @@ GEXTEND Gram
     [ [ l = LIST1 qualidarg -> l ] ]
   ;
   ne_qualidconstarg_list:
-    [ [ l = LIST1 qualidarg -> l ] ]
+    [ [ l = LIST1 qualidconstarg -> l ] ]
   ;
   ne_num_list:
     [ [ n = numarg; l = ne_num_list -> n :: l | n = numarg -> [n] ] ]
-- 
cgit v1.2.3