diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-10 15:04:13 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-10 15:53:06 +0200 |
commit | 0acaa906367c02c57a6d70dd5d19eaea884b7568 (patch) | |
tree | 12cf860589f0d32db04610771752d6022a0c01d9 /interp/notation.mli | |
parent | dfa99b152114271cf9fac4cab9d8663ac6ec078c (diff) |
Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).
Diffstat (limited to 'interp/notation.mli')
-rw-r--r-- | interp/notation.mli | 4 |
1 files changed, 2 insertions, 2 deletions
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} *) |