diff options
| author | herbelin | 2002-11-25 11:09:14 +0000 |
|---|---|---|
| committer | herbelin | 2002-11-25 11:09:14 +0000 |
| commit | ba259b0653108ae9cccf5c8dacafcc5ee73a1a23 (patch) | |
| tree | 0485304602457a25c095a83e7e01742ae386b9bf | |
| parent | 34deee50de7a2b890462ceca4f7f203b6076863e (diff) | |
Retour sur le choix des delimiteurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3275 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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) |