From f3d34e3e3add974d79d14f043c19a6d76c2b71b7 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 23 Sep 2003 11:22:20 +0000 Subject: Utilisation de noms dans 'Implicit Arguments [...]' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4459 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/g_vernacnew.ml4 | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'parsing/g_vernacnew.ml4') diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 4c096964d..cca57911b 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -436,8 +436,9 @@ GEXTEND Gram VernacNotation (false,c,Some("'"^id^"'",[]),None,None) *) | IDENT "Implicit"; IDENT "Arguments"; qid = global; - pos = OPT [ "["; l = LIST0 natural; "]" -> l ] -> - VernacDeclareImplicits (qid,pos) + pos = OPT [ "["; l = LIST0 ident; "]" -> l ] -> + let pos = option_app (List.map (fun id -> ExplByName id)) pos in + VernacDeclareImplicits (qid,pos) | IDENT "Implicit"; ["Type" | "Types"]; idl = LIST1 ident; ":"; c = lconstr -> VernacReserve (idl,c) @@ -681,7 +682,7 @@ GEXTEND Gram "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl) | IDENT "Infix"; local = locality; (*a = entry_prec; n = OPT natural; *) - op = STRING; p = global; + op = STRING; ":="; p = global; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> let (a,n,b) = Metasyntax.interp_infix_modifiers None None modl in -- cgit v1.2.3