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 e63ad10cd..5f6bfa35f 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -21,7 +21,7 @@ open Ppextend (** A scope is a set of interpreters for symbols + optional interpreter and printers for integers + optional delimiters *) -type level = precedence * tolerability list +type level = precedence * tolerability list * notation_var_internalization_type list type delimiters = string type scope type scopes (** = [scope_name list] *) |