diff options
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 7a8f824780..1d7519c99f 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -403,11 +403,10 @@ GEXTEND Gram Pp.warning "Class is obsolete"; VernacNop (* Implicit *) -(* | IDENT "Syntactic"; "Definition"; id = base_ident; ":="; c = constr; n = OPT [ "|"; n = natural -> n ] -> VernacSyntacticDefinition (id,c,n) -*) +(* | IDENT "Syntactic"; "Definition"; id = IDENT; ":="; c = constr; n = OPT [ "|"; n = natural -> n ] -> let c = match n with @@ -416,7 +415,7 @@ GEXTEND Gram CApp (loc,c,l) | None -> c in VernacNotation ("'"^id^"'",c,[],None) - +*) | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" -> VernacDeclareImplicits (qid,Some l) | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None) |