From 125c2ade92dbdd891c86850e9710a1f203c4ec3c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 20 Nov 2000 09:05:35 +0000
Subject: Prise en compte des noms qualifiés dans certaines commandes

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

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index a3145ca04d..0a7c0586b3 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -310,9 +310,9 @@ GEXTEND Gram
       | IDENT "End"; id = identarg; "." -> <:ast< (EndSection $id) >>
 
 (* Transparent and Opaque *)
-      | IDENT "Transparent"; l = ne_identarg_list; "." ->
+      | IDENT "Transparent"; l = ne_qualidconstarg_list; "." ->
           <:ast< (TRANSPARENT ($LIST $l)) >>
-      | IDENT "Opaque"; l = ne_identarg_list; "." -> 
+      | IDENT "Opaque"; l = ne_qualidconstarg_list; "." -> 
 	  <:ast< (OPAQUE ($LIST $l)) >>
 
 (* Coercions *)
-- 
cgit v1.2.3