From 53e19f76624b7a18792af799e970e9478f8e90a9 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 16 Jun 2020 17:09:40 +0200
Subject: Fix #11121: Simultaneous definition of term and notation in custom
 grammar

---
 interp/notation.mli | 22 +++++++++++++++++++---
 1 file changed, 19 insertions(+), 3 deletions(-)

(limited to 'interp/notation.mli')

diff --git a/interp/notation.mli b/interp/notation.mli
index e7e917463b..c39bfa6e28 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -298,8 +298,8 @@ type symbol =
 val symbol_eq : symbol -> symbol -> bool
 
 (** Make/decompose a notation of the form "_ U _" *)
-val make_notation_key : notation_entry_level -> symbol list -> notation
-val decompose_notation_key : notation -> notation_entry_level * symbol list
+val make_notation_key : notation_entry -> symbol list -> notation
+val decompose_notation_key : notation -> notation_entry * symbol list
 
 (** Decompose a notation of the form "a 'U' b" *)
 val decompose_raw_notation : string -> symbol list
@@ -313,8 +313,10 @@ val locate_notation : (glob_constr -> Pp.t) -> notation_key ->
 
 val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t
 
+val make_notation_entry_level : notation_entry -> entry_level -> notation_entry_level
+
 type entry_coercion = (notation_with_optional_scope * notation) list
-val declare_entry_coercion : specific_notation -> notation_entry_level -> unit
+val declare_entry_coercion : specific_notation -> entry_level option -> notation_entry_level -> unit
 val availability_of_entry_coercion : notation_entry_level -> notation_entry_level -> entry_coercion option
 
 val declare_custom_entry_has_global : string -> int -> unit
@@ -323,6 +325,20 @@ val declare_custom_entry_has_ident : string -> int -> unit
 val entry_has_global : notation_entry_level -> bool
 val entry_has_ident : notation_entry_level -> bool
 
+(** Dealing with precedences *)
+
+type level = notation_entry * entry_level * entry_relative_level list
+  (* first argument is InCustomEntry s for custom entries *)
+
+val level_eq : level -> level -> bool
+val entry_relative_level_eq : entry_relative_level -> entry_relative_level -> bool
+
+(** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
+
+val declare_notation_level : notation -> level -> unit
+val level_of_notation : notation -> level
+  (** raise [Not_found] if not declared *)
+
 (** Rem: printing rules for primitive token are canonical *)
 
 val with_notation_protection : ('a -> 'b) -> 'a -> 'b
-- 
cgit v1.2.3