From 9bc339f529fc2ee2389a717914514829a73686bc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 24 Sep 2018 23:14:29 +0200
Subject: Fixing #8551 (missing delimiters when notation exists both lonely and
 in 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 8cc69f4d1b..3480d1c8f2 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -219,6 +219,7 @@ type notation_rule_core =
 type notation_rule =
     notation_rule_core
   * delimiters option (* delimiter to possibly add *)
+  * bool (* true if the delimiter is mandatory *)
 
 (** Return the possible notations for a given term *)
 val uninterp_notations : subscopes -> 'a glob_constr_g -> notation_rule list
-- 
cgit v1.2.3