6 files changed, 35 insertions, 39 deletions
diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
index 9f133ca9d4..427505c199 100644
--- a/parsing/notation_gram.ml
+++ b/parsing/notation_gram.ml
@@ -10,14 +10,11 @@
 
 open Names
 open Extend
+open Constrexpr
 
 (** Dealing with precedences *)
 
-type precedence = int
-type parenRelation = L | E | Any | Prec of precedence
-type tolerability = precedence * parenRelation
-
-type level = Constrexpr.notation_entry * precedence * tolerability list * constr_entry_key list
+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 =
@@ -37,7 +34,4 @@ type one_notation_grammar = {
   notgram_prods : grammar_constr_prod_item list list;
 }
 
-type notation_grammar = {
-  notgram_onlyprinting : bool;
-  notgram_rules : one_notation_grammar list
-}
+type notation_grammar = one_notation_grammar list
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 661f9c5cad..b6699493bb 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -12,19 +12,19 @@ open Pp
 open CErrors
 open Util
 open Notation
-open Notation_gram
+open Constrexpr
 
 (* Register the level of notation for parsing and printing
-   (we also register a precomputed parsing rule) *)
+   (also register the parsing rule if not onlyprinting) *)
 
 let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
 
-let declare_notation_level ntn ~onlyprint parsing_rule level =
+let declare_notation_level ntn parsing_rule level =
   try
     let _ = NotationMap.find ntn !notation_level_map in
     anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.")
   with Not_found ->
-  notation_level_map := NotationMap.add ntn (onlyprint,parsing_rule,level) !notation_level_map
+  notation_level_map := NotationMap.add ntn (parsing_rule,level) !notation_level_map
 
 let level_of_notation ntn =
   NotationMap.find ntn !notation_level_map
@@ -37,10 +37,11 @@ let get_defined_notations () =
 
 open Extend
 
-let parenRelation_eq t1 t2 = match t1, t2 with
-| L, L | E, E | Any, Any -> true
-| Prec l1, Prec l2 -> Int.equal l1 l2
-| _ -> false
+let entry_relative_level_eq t1 t2 = match t1, t2 with
+| LevelLt n1, LevelLt n2 -> Int.equal n1 n2
+| LevelLe n1, LevelLe n2 -> Int.equal n1 n2
+| LevelSome, LevelSome -> true
+| (LevelLt _ | LevelLe _ | LevelSome), _ -> false
 
 let production_position_eq pp1 pp2 = match (pp1,pp2) with
 | BorderProd (side1,assoc1), BorderProd (side2,assoc2) -> side1 = side2 && assoc1 = assoc2
@@ -64,11 +65,10 @@ let constr_entry_key_eq eq v1 v2 = match v1, v2 with
 | (ETIdent | ETGlobal | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
 
 let level_eq_gen strict (s1, l1, t1, u1) (s2, l2, t2, u2) =
-  let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
   let prod_eq (l1,pp1) (l2,pp2) =
     not strict ||
     (production_level_eq l1 l2 && production_position_eq pp1 pp2) in
-  notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal tolerability_eq t1 t2
+  notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal entry_relative_level_eq t1 t2
   && List.equal (constr_entry_key_eq prod_eq) u1 u2
 
 let level_eq = level_eq_gen false
diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli
index d5711569f0..d8b7e8e4c1 100644
--- a/parsing/notgram_ops.mli
+++ b/parsing/notgram_ops.mli
@@ -13,11 +13,12 @@ open Constrexpr
 open Notation_gram
 
 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 -> onlyprint:bool -> notation_grammar -> level -> unit
-val level_of_notation : notation -> bool (* = onlyprint *) * notation_grammar * level
+val declare_notation_level : notation -> notation_grammar option -> level -> unit
+val level_of_notation : notation -> notation_grammar option * level
   (** raise [Not_found] if not declared *)
 
 (** Returns notations with defined parsing/printing rules *)
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index 2154f2f881..12311f9cd9 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -2,8 +2,8 @@ Tok
 CLexer
 Extend
 Notation_gram
-Ppextend
 Notgram_ops
+Ppextend
 Pcoq
 G_constr
 G_prim
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index 92f44faec8..393ab8a302 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -12,7 +12,8 @@ open Util
 open Pp
 open CErrors
 open Notation
-open Notation_gram
+open Constrexpr
+open Notgram_ops
 
 (*s Pretty-print. *)
 
@@ -37,29 +38,30 @@ let ppcmd_of_cut = function
   | PpBrk(n1,n2) -> brk(n1,n2)
 
 type unparsing =
-  | UnpMetaVar of int * parenRelation
-  | UnpBinderMetaVar of int * parenRelation
-  | UnpListMetaVar of int * parenRelation * unparsing list
-  | UnpBinderListMetaVar of int * bool * unparsing list
+  | UnpMetaVar of entry_relative_level
+  | UnpBinderMetaVar of entry_relative_level
+  | UnpListMetaVar of entry_relative_level * unparsing list
+  | UnpBinderListMetaVar of bool * unparsing list
   | UnpTerminal of string
   | UnpBox of ppbox * unparsing Loc.located list
   | UnpCut of ppcut
 
-type unparsing_rule = unparsing list * precedence
+type unparsing_rule = unparsing list * entry_level
 type extra_unparsing_rules = (string * string) list
 
 let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with
-  | UnpMetaVar (n1,p1), UnpMetaVar (n2,p2) -> n1 = n2 && p1 = p2
-  | UnpBinderMetaVar (n1,p1), UnpBinderMetaVar (n2,p2) -> n1 = n2 && p1 = p2
-  | UnpListMetaVar (n1,p1,l1), UnpListMetaVar (n2,p2,l2) -> n1 = n2 && p1 = p2 && List.for_all2eq unparsing_eq l1 l2
-  | UnpBinderListMetaVar (n1,b1,l1), UnpBinderListMetaVar (n2,b2,l2) -> n1 = n2 && b1 = b2 && List.for_all2eq unparsing_eq l1 l2
+  | UnpMetaVar p1, UnpMetaVar p2 -> entry_relative_level_eq p1 p2
+  | UnpBinderMetaVar p1, UnpBinderMetaVar p2 -> entry_relative_level_eq p1 p2
+  | UnpListMetaVar (p1,l1), UnpListMetaVar (p2,l2) -> entry_relative_level_eq p1 p2 && List.for_all2eq unparsing_eq l1 l2
+  | UnpBinderListMetaVar (b1,l1), UnpBinderListMetaVar (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq l1 l2
   | UnpTerminal s1, UnpTerminal s2 -> String.equal s1 s2
   | UnpBox (b1,l1), UnpBox (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq (List.map snd l1) (List.map snd l2)
   | UnpCut p1, UnpCut p2 -> p1 = p2
   | (UnpMetaVar _ | UnpBinderMetaVar _ | UnpListMetaVar _ |
      UnpBinderListMetaVar _ | UnpTerminal _ | UnpBox _ | UnpCut _), _ -> false
 
-(* Concrete syntax for symbolic-extension table *)
+(* Register generic and specific printing rules *)
+
 let generic_notation_printing_rules =
   Summary.ref ~name:"generic-notation-printing-rules" (NotationMap.empty : (unparsing_rule * bool * extra_unparsing_rules) NotationMap.t)
 
diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli
index 7996e7696d..346fc83f5f 100644
--- a/parsing/ppextend.mli
+++ b/parsing/ppextend.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Constrexpr
-open Notation_gram
 
 (** {6 Pretty-print. } *)
 
@@ -31,15 +30,15 @@ val ppcmd_of_cut : ppcut -> Pp.t
 
 (** Declare and look for the printing rule for symbolic notations *)
 type unparsing =
-  | UnpMetaVar of int * parenRelation
-  | UnpBinderMetaVar of int * parenRelation
-  | UnpListMetaVar of int * parenRelation * unparsing list
-  | UnpBinderListMetaVar of int * bool * unparsing list
+  | UnpMetaVar of entry_relative_level
+  | UnpBinderMetaVar of entry_relative_level
+  | UnpListMetaVar of entry_relative_level * unparsing list
+  | UnpBinderListMetaVar of bool * unparsing list
   | UnpTerminal of string
   | UnpBox of ppbox * unparsing Loc.located list
   | UnpCut of ppcut
 
-type unparsing_rule = unparsing list * precedence
+type unparsing_rule = unparsing list * entry_level
 type extra_unparsing_rules = (string * string) list
 
 val unparsing_eq : unparsing -> unparsing -> bool