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

---
 parsing/notation_gram.ml | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

(limited to 'parsing/notation_gram.ml')

diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
index 7940931dfc..045f497070 100644
--- a/parsing/notation_gram.ml
+++ b/parsing/notation_gram.ml
@@ -9,13 +9,6 @@
 (************************************************************************)
 
 open Names
-open Extend
-open Constrexpr
-
-(** Dealing with precedences *)
-
-type level = notation_entry * entry_level * entry_relative_level list * constr_entry_key list
-  (* first argument is InCustomEntry s for custom entries *)
 
 type grammar_constr_prod_item =
   | GramConstrTerminal of string Tok.p
@@ -28,10 +21,11 @@ type grammar_constr_prod_item =
 (** Grammar rules for a notation *)
 
 type one_notation_grammar = {
-  notgram_level : level;
+  notgram_level : Notation.level;
   notgram_assoc : Gramlib.Gramext.g_assoc option;
   notgram_notation : Constrexpr.notation;
   notgram_prods : grammar_constr_prod_item list list;
+  notgram_typs : Extend.constr_entry_key list;
 }
 
 type notation_grammar = one_notation_grammar list
-- 
cgit v1.2.3