diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 4865611a6..629c20177 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -424,7 +424,7 @@ GEXTEND Gram let l = list_tabulate (fun _ -> (CHole (loc),None)) n in CApp (loc,c,l) | None -> c in - VernacNotation (false,"'"^id^"'",c,[],None,None) + VernacNotation (false,c,Some("'"^id^"'",[]),None,None) | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" -> VernacDeclareImplicits (qid,Some l) | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None) |