From c6c45dea6fa60516f94b8053c9d4a8ee340cabfd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 24 Sep 2003 08:48:54 +0000
Subject: Utilisation de noms dans 'Implicit Arguments [...]'

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

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d52ced8171..16d2ba9c57 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -427,6 +427,7 @@ GEXTEND Gram
 	     | None -> c in
 	   VernacNotation (false,c,Some("'"^id^"'",[]),None,None)
       | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
+	  let l = List.map (fun n -> ExplByPos n) l in
 	  VernacDeclareImplicits (qid,Some l)
       | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None)
 
-- 
cgit v1.2.3