From f442efebd8354b233827e4991a80d27082c772e1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 24 Jul 2017 20:04:46 +0200
Subject: A little reorganization of notations + a fix to #5608.

- Formerly, notations such as "{ A } + { B }" were typically split
  into "{ _ }" and "_ + _". We keep the split only for parsing, which
  is where it is really needed, but not anymore for interpretation,
  nor printing.
- As a consequence, one notation string can give rise to several
  grammar entries, but still only one printing entry.
- As another consequence, "{ A } + { B }" and "A + { B }" must be
  reserved to be used, which is after all the natural expectation,
  even if the sublevels are constrained.
- We also now keep the information "is ident", "is binder" in the
  "key" characterizing the level of a notation.
---
 intf/notation_term.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'intf/notation_term.ml')

diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index cee96040bd..084a1042c7 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -88,11 +88,12 @@ 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 = {
+type one_notation_grammar = {
   notgram_level : int;
   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;
-  notgram_onlyprinting : bool;
 }
+
+type notation_grammar = (* onlyprinting *) bool * one_notation_grammar list
-- 
cgit v1.2.3


From 5db048b7f9cb5d13e44d87a1007ff042eef25fb5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 24 Jul 2017 21:01:23 +0200
Subject: A new step of restructuration of notations.

This allows to issue a more appropriate message when a notation with a
{ } cannot be defined because of an incompatible level. E.g.:

Notation "{ A } + B" := (sumbool A B) (at level 20).
---
 intf/notation_term.ml | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

(limited to 'intf/notation_term.ml')

diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index 084a1042c7..c342da3dca 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -88,12 +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 *)
 
+(** 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 : int;
+  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 = (* onlyprinting *) bool * one_notation_grammar list
+type notation_grammar = {
+  notgram_onlyprinting : bool;
+  notgram_rules : one_notation_grammar list
+}
-- 
cgit v1.2.3