diff options
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index a67948a778..b32561d908 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -217,7 +217,8 @@ type interp_rule = | SynDefRule of KerName.t val declare_notation_interpretation : notation -> scope_name option -> - interpretation -> notation_location -> onlyprint:bool -> unit + interpretation -> notation_location -> onlyprint:bool -> + Deprecation.t option -> unit val declare_uninterpretation : interp_rule -> interpretation -> unit |