From d62444ef6ffc8bce549b53b2ccfaaae3e630e80c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 16 Feb 2001 13:48:02 +0000
Subject: Prise en compte noms longs dans Implicits

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

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 36d7c3a7cb..431b687f69 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -371,10 +371,10 @@ GEXTEND Gram
           <:ast< (IMPLICIT_ARGS_ON) >>
       | IDENT "Implicit"; IDENT "Arguments"; IDENT "Off" ->
           <:ast< (IMPLICIT_ARGS_OFF) >>
-      | IDENT "Implicits"; id = identarg; "["; l = numarg_list; "]" ->
-          <:ast< (IMPLICITS "" $id ($LIST $l)) >>
-      | IDENT "Implicits"; id = identarg ->
-          <:ast< (IMPLICITS "Auto" $id) >> 
+      | IDENT "Implicits"; qid = qualidarg; "["; l = numarg_list; "]" ->
+          <:ast< (IMPLICITS "" $qid ($LIST $l)) >>
+      | IDENT "Implicits"; qid = qualidarg ->
+          <:ast< (IMPLICITS "Auto" $qid) >> 
   ] ]
   ;
 END
-- 
cgit v1.2.3