diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-23 11:22:20 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-23 11:22:20 +0000 |
| commit | f3d34e3e3add974d79d14f043c19a6d76c2b71b7 (patch) | |
| tree | 261ca12f9f18fcbb530ce18d9928ff369b7a41cd /parsing/g_vernacnew.ml4 | |
| parent | 87ab5e4f9a4f93d152df721f97a0bcb6cddef973 (diff) | |
Utilisation de noms dans 'Implicit Arguments [...]'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4459 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_vernacnew.ml4')
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 7 |
1 files changed, 4 insertions, 3 deletions
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 |