Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructuration

1 files changed, 16 insertions, 3 deletions

diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index cee96040bd..c342da3dca 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -88,11 +88,24 @@ type grammar_constr_prod_item =
        concat with last parsed list when true; additionally release
        the p last items as if they were parsed autonomously *)
 
-type notation_grammar = {
-  notgram_level : int;
+(** Dealing with precedences *)
+
+type precedence = int
+type parenRelation = L | E | Any | Prec of precedence
+type tolerability = precedence * parenRelation
+
+type level = precedence * tolerability list * notation_var_internalization_type list
+
+(** Grammar rules for a notation *)
+
+type one_notation_grammar = {
+  notgram_level : level;
   notgram_assoc : Extend.gram_assoc option;
   notgram_notation : Constrexpr.notation;
   notgram_prods : grammar_constr_prod_item list list;
-  notgram_typs : notation_var_internalization_type list;
+}
+
+type notation_grammar = {
   notgram_onlyprinting : bool;
+  notgram_rules : one_notation_grammar list
 }