diff options
| author | Pierre-Marie Pédrot | 2016-06-27 23:41:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-28 01:19:46 +0200 |
| commit | 64e7be2e88f01ad65928e4b2b537e60c2c4e9260 (patch) | |
| tree | c653d6f9a2aebf573fd463bf02ce6ecb80ccdc04 /interp/notation.mli | |
| parent | 9f9c1dc37ca3ffe30417c8f7b63d62ad5b63e51b (diff) | |
Properly handling the only printing flag when parsing rules already exist.
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index a85dc50f2f..b47e1975e3 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -109,7 +109,7 @@ type interp_rule = | SynDefRule of kernel_name val declare_notation_interpretation : notation -> scope_name option -> - interpretation -> notation_location -> unit + interpretation -> notation_location -> onlyprint:bool -> unit val declare_uninterpretation : interp_rule -> interpretation -> unit |