diff options
| -rw-r--r-- | parsing/g_basevernac.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 55a3504471..d042f8c915 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -226,7 +226,7 @@ GEXTEND Gram | IDENT "Open"; IDENT "Scope"; sc = IDENT -> VernacOpenScope sc | IDENT "Delimits"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT -> - VernacDelimiters (sc,("`"^key^":","`")) + VernacDelimiters (sc,("'"^key^":","'")) | IDENT "Arguments"; IDENT "Scope"; qid = global; "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl) |