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 3480d1c8f2..ab0501a1e1 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -54,7 +54,7 @@ val scope_is_open : scope_name -> bool (** Open scope *) val open_close_scope : - (** locality *) bool * (* open *) bool * scope_name -> unit + (* locality *) bool * (* open *) bool * scope_name -> unit (** Extend a list of scopes *) val empty_scope_stack : scopes |