diff options
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 25ea594190..de14c95155 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -178,3 +178,5 @@ val declare_notation_printing_rule : notation -> unparsing_rule -> unit val find_notation_printing_rule : notation -> unparsing_rule (** Rem: printing rules for primitive token are canonical *) + +val with_notation_protection : ('a -> 'b) -> 'a -> 'b |