diff options
Diffstat (limited to 'intf/vernacexpr.mli')
| -rw-r--r-- | intf/vernacexpr.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 6ce15a7c5..cfa30a4d5 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -206,6 +206,7 @@ type syntax_modifier = | SetAssoc of Extend.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key | SetOnlyParsing of Flags.compat_version + | SetOnlyPrinting | SetFormat of string * string located type proof_end = |