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 21d3ae1a08..57e0deb10a 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -167,7 +167,8 @@ val decompose_notation_key : notation -> symbol list (* Prints scopes (expect a pure aconstr printer *) val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds -val locate_notation : (rawconstr -> std_ppcmds) -> notation -> std_ppcmds +val locate_notation : (rawconstr -> std_ppcmds) -> notation -> + scope_name option -> std_ppcmds val pr_visibility: (rawconstr -> std_ppcmds) -> scope_name option -> std_ppcmds |