From aac2d2ac490492f8466e1d45ba0079de376fe25a Mon Sep 17 00:00:00 2001
From: Lionel Rieg
Date: Thu, 25 Jun 2015 14:58:25 +0200
Subject: Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"

---
 interp/notation.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'interp/notation.mli')

diff --git a/interp/notation.mli b/interp/notation.mli
index 854c52b2c7..38bd5fc7b8 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -55,6 +55,7 @@ val find_scope : scope_name -> scope
 (** Declare delimiters for printing *)
 
 val declare_delimiters : scope_name -> delimiters -> unit
+val remove_delimiters : scope_name -> unit
 val find_delimiters_scope : Loc.t -> delimiters -> scope_name
 
 (** {6 Declare and uses back and forth an interpretation of primitive token } *)
-- 
cgit v1.2.3