diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index d79b3ec3a8..ad3862388e 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -418,14 +418,14 @@ GEXTEND Gram n = OPT [ "|"; n = natural -> n ] -> VernacSyntacticDefinition (id,c,n) *) - | IDENT "Syntactic"; "Definition"; id = IDENT; ":="; c = constr; + | IDENT "Syntactic"; "Definition"; id = ident; ":="; c = constr; n = OPT [ "|"; n = natural -> n ] -> let c = match n with | Some n -> let l = list_tabulate (fun _ -> (CHole (loc),None)) n in CApp (loc,(None,c),l) | None -> c in - VernacNotation (false,c,Some("'"^id^"'",[]),None,None) + VernacSyntacticDefinition (id,c,false,true) | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" -> let l = List.map (fun n -> ExplByPos n) l in VernacDeclareImplicits (qid,Some l) |