diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index e670f68c21..2c73a974b5 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -206,7 +206,7 @@ type syntax_modifier = | SetAssoc of Extend.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key | SetOnlyParsing of Flags.compat_version - | SetFormat of string located + | SetFormat of string * string located type proof_end = | Admitted @@ -290,6 +290,7 @@ type vernac_expr = | VernacNotation of obsolete_locality * constr_expr * (lstring * syntax_modifier list) * scope_name option + | VernacNotationAddFormat of string * string * string (* Gallina *) | VernacDefinition of |