diff options
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index f3036f226f..3dc3c95c20 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -164,7 +164,7 @@ type symbol = val make_notation_key : symbol list -> notation val decompose_notation_key : notation -> symbol list -(* Prints scopes (expect a pure aconstr printer *) +(* Prints scopes (expects 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 -> |