diff options
| author | Pierre-Marie Pédrot | 2016-06-06 17:08:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-07 15:54:22 +0200 |
| commit | d7737ba9b3a811b8415ce87d8e3e091c9e49d32e (patch) | |
| tree | e0ae4f5739bd6e49fe5827da38e800913b2c9712 /intf | |
| parent | 5520db62486ad628f91737833623aa69c4c1b8af (diff) | |
Adding an only printing flag to notations.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/notation_term.mli | 1 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/intf/notation_term.mli b/intf/notation_term.mli index c7c301629e..883b017727 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.mli @@ -92,4 +92,5 @@ type notation_grammar = { notgram_notation : Constrexpr.notation; notgram_prods : grammar_constr_prod_item list list; notgram_typs : notation_var_internalization_type list; + notgram_onlyprinting : bool; } diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index ae9328fcc0..0e37f5268e 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 = |