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"

---
 intf/vernacexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index d7b269a1de..0ca3bb35f6 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -284,7 +284,7 @@ type vernac_expr =
   | VernacSyntaxExtension of
       obsolete_locality * (lstring * syntax_modifier list)
   | VernacOpenCloseScope of obsolete_locality * (bool * scope_name)
-  | VernacDelimiters of scope_name * string
+  | VernacDelimiters of scope_name * string option
   | VernacBindScope of scope_name * reference or_by_notation list
   | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) *
       constr_expr * scope_name option
-- 
cgit v1.2.3