From 821a7ed17bc5e474b1f1a34bce24ba40c28b5388 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 13 Sep 2001 15:50:54 +0000
Subject: Prise en compte qualid dans Hint Unfold

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

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index ae1c925996..9d6455608b 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -138,7 +138,7 @@ GEXTEND Gram
 	  <:ast<(HintImmediate $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
 	  
       | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
-	IDENT "Unfold"; c = identarg ->
+	IDENT "Unfold"; c = qualidarg ->
 	  <:ast<(HintUnfold $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
 	  
       | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
-- 
cgit v1.2.3