diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/symbols.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/symbols.mli b/interp/symbols.mli index 0f13c0d57e..1f5bc2607c 100644 --- a/interp/symbols.mli +++ b/interp/symbols.mli @@ -103,8 +103,8 @@ val availability_of_notation : scope_name * notation -> scopes -> (*s Declare and test the level of a (possibly uninterpreted) notation *) -val declare_notation_level : notation -> level -> unit -val level_of_notation : notation -> level (* [Not_found] if no level *) +val declare_notation_level : notation -> level option * level -> unit +val level_of_notation : notation -> level option * level (* [Not_found] if no level *) (*s** Miscellaneous *) |