diff options
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 |