aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_basevernac.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_basevernac.ml4')
-rw-r--r--parsing/g_basevernac.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 0d27fc759..14f1061ed 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -368,7 +368,7 @@ GEXTEND Gram
| IDENT "no"; IDENT "associativity" -> SetAssoc Gramext.NonA
| x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ)
| IDENT "only"; IDENT "parsing" -> SetOnlyParsing
- | IDENT "format"; s = STRING -> SetFormat s ] ]
+ | IDENT "format"; s = [s = STRING -> (loc,s)] -> SetFormat s ] ]
;
syntax_extension_type:
[ [ IDENT "ident" -> ETIdent | IDENT "global" -> ETReference