From 0acaa906367c02c57a6d70dd5d19eaea884b7568 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 10 May 2018 15:04:13 +0200 Subject: Fixes #7462, part 2 (only-printing not make believe parsing rule is declared). --- interp/notation.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'interp/notation.mli') diff --git a/interp/notation.mli b/interp/notation.mli index eac87414f..ccc67fe49 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -137,8 +137,8 @@ val availability_of_notation : scope_name option * notation -> local_scopes -> (** {6 Declare and test the level of a (possibly uninterpreted) notation } *) -val declare_notation_level : notation -> level -> unit -val level_of_notation : notation -> level (** raise [Not_found] if no level *) +val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit +val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *) (** {6 Miscellaneous} *) -- cgit v1.2.3