diff options
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 19a03a22e6..4c62250d23 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -693,7 +693,7 @@ GEXTEND Gram | IDENT "Uninterpreted"; IDENT "Notation"; local = locality; s = STRING; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] - -> VernacSyntaxExtension (local,s,l) + -> VernacSyntaxExtension (local,s,l,None) (* "Print" "Grammar" should be here but is in "command" entry in order to factorize with other "Print"-based vernac entries *) |