diff options
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 5f6bfa35f..f9f247fe1 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -21,7 +21,6 @@ open Ppextend (** A scope is a set of interpreters for symbols + optional interpreter and printers for integers + optional delimiters *) -type level = precedence * tolerability list * notation_var_internalization_type list type delimiters = string type scope type scopes (** = [scope_name list] *) |