diff options
Diffstat (limited to 'toplevel/metasyntax.mli')
| -rw-r--r-- | toplevel/metasyntax.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 38a37757..f22839f4 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -39,6 +39,7 @@ val add_notation_extra_printing_rule : string -> string -> string -> unit (** Declaring delimiter keys and default scopes *) val add_delimiters : scope_name -> string -> unit +val remove_delimiters : scope_name -> unit val add_class_scope : scope_name -> scope_class list -> unit (** Add only the interpretation of a notation that already has pa/pp rules *) |