Merge PR #11635: Cleanup around the tolerability structure

Reviewed-by: ejgallego

21 files changed, 237 insertions, 228 deletions

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index cb6e695865..42dd2dd052 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -2,6 +2,12 @@
 
 ### ML API
 
+Types `precedence`, `parenRelation`, `tolerability` in
+`notgram_ops.ml` have been reworked. See `entry_level` and
+`entry_relative_level` in `constrexpr.ml`.
+
+### ML API
+
 Exception handling:
 
 - Coq's custom `Backtrace` module has been removed in favor of OCaml's
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 1d51109b7f..4bdacda529 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -20,8 +20,12 @@ type ident_decl = lident * universe_decl_expr option
 type name_decl = lname * universe_decl_expr option
 
 type notation_with_optional_scope = LastLonelyNotation | NotationInScope of string
+
+type entry_level = int
+type entry_relative_level = LevelLt of entry_level | LevelLe of entry_level | LevelSome
+
 type notation_entry = InConstrEntry | InCustomEntry of string
-type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * int
+type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * entry_level
 type notation_key = string
 
 (* A notation associated to a given parsing rule *)
diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
index ffc92fa53a..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 =
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index a84d2a4cb0..b6699493bb 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -12,7 +12,7 @@ open Pp
 open CErrors
 open Util
 open Notation
-open Notation_gram
+open Constrexpr
 
 (* Register the level of notation for parsing and printing
    (also register the parsing rule if not onlyprinting) *)
@@ -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 7c676fbb10..d8b7e8e4c1 100644
--- a/parsing/notgram_ops.mli
+++ b/parsing/notgram_ops.mli
@@ -13,6 +13,7 @@ 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 } *)
 
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 0277e79adb..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,22 +38,22 @@ 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
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
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index bab6bfd78e..5835d75c79 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -298,7 +298,7 @@ END
 let pr_by_arg_tac env sigma _prc _prlc prtac opt_c =
   match opt_c with
     | None -> mt ()
-    | Some t -> hov 2 (str "by" ++ spc () ++ prtac env sigma (3,Notation_gram.E) t)
+    | Some t -> hov 2 (str "by" ++ spc () ++ prtac env sigma (Constrexpr.LevelLe 3) t)
 
 }
 
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 6dd51e4e01..dd4195f2ef 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -67,7 +67,7 @@ val wit_by_arg_tac :
 
 val pr_by_arg_tac :
   Environ.env -> Evd.evar_map ->
-  (Environ.env -> Evd.evar_map -> int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) ->
+  (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> raw_tactic_expr -> Pp.t) ->
   raw_tactic_expr option -> Pp.t
 
 val test_lpar_id_colon : unit Pcoq.Entry.t
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 7843faaef3..e2b8bcb5a9 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -17,7 +17,6 @@ open Constrexpr
 open Genarg
 open Geninterp
 open Stdarg
-open Notation_gram
 open Tactypes
 open Locus
 open Genredexpr
@@ -73,43 +72,43 @@ type 'a raw_extra_genarg_printer =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) ->
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) ->
   'a -> Pp.t
 
 type 'a glob_extra_genarg_printer =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) ->
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) ->
   'a -> Pp.t
 
 type 'a extra_genarg_printer =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) ->
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) ->
   'a -> Pp.t
 
 type 'a raw_extra_genarg_printer_with_level =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) ->
-  tolerability -> 'a -> Pp.t
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) ->
+  entry_relative_level -> 'a -> Pp.t
 
 type 'a glob_extra_genarg_printer_with_level =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) ->
-  tolerability -> 'a -> Pp.t
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) ->
+  entry_relative_level -> 'a -> Pp.t
 
 type 'a extra_genarg_printer_with_level =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) ->
-  tolerability -> 'a -> Pp.t
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) ->
+  entry_relative_level -> 'a -> Pp.t
 
 let string_of_genarg_arg (ArgumentType arg) =
   let rec aux : type a b c. (a, b, c) genarg_type -> string = function
@@ -294,7 +293,7 @@ let string_of_genarg_arg (ArgumentType arg) =
       let pr _ = str "_" in
       KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)"
 
-  let pr_farg prtac arg = prtac (1, Any) (TacArg (CAst.make arg))
+  let pr_farg prtac arg = prtac LevelSome (TacArg (CAst.make arg))
 
   let is_genarg tag wit =
     let ArgT.Any tag = tag in
@@ -314,35 +313,35 @@ let string_of_genarg_arg (ArgumentType arg) =
 
   let rec pr_any_arg : type l. (_ -> l generic_argument -> Pp.t) -> _ -> l generic_argument -> Pp.t =
   fun prtac symb arg -> match symb with
-  | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac (1, Any) arg
+  | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac LevelSome arg
   | Extend.Ulist1 s | Extend.Ulist0 s ->
     begin match get_list arg with
-    | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+    | None -> str "ltac:(" ++ prtac LevelSome arg ++ str ")"
     | Some l -> pr_sequence (pr_any_arg prtac s) l
     end
   | Extend.Ulist1sep (s, sep) | Extend.Ulist0sep (s, sep) ->
     begin match get_list arg with
-    | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+    | None -> str "ltac:(" ++ prtac LevelSome arg ++ str ")"
     | Some l -> prlist_with_sep (fun () -> str sep) (pr_any_arg prtac s) l
     end
   | Extend.Uopt s ->
     begin match get_opt arg with
-    | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+    | None -> str "ltac:(" ++ prtac LevelSome arg ++ str ")"
     | Some l -> pr_opt (pr_any_arg prtac s) l
     end
   | Extend.Uentry _ | Extend.Uentryl _ ->
-    str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+    str "ltac:(" ++ prtac LevelSome arg ++ str ")"
 
   let pr_targ prtac symb arg = match symb with
   | Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) ->
-    prtac (1, Any) arg
-  | Extend.Uentryl (_, l) -> prtac (l, Any) arg
+    prtac LevelSome arg
+  | Extend.Uentryl (_, l) -> prtac LevelSome arg
   | _ ->
     match arg with
     | TacGeneric arg ->
       let pr l arg = prtac l (TacGeneric arg) in
       pr_any_arg pr symb arg
-    | _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+    | _ -> str "ltac:(" ++ prtac LevelSome arg ++ str ")"
 
   let pr_raw_extend_rec prtac =
     pr_extend_gen (pr_farg prtac)
@@ -630,7 +629,7 @@ let pr_goal_selector ~toplevel s =
 
   let pr_then () = str ";"
 
-  let ltop = (5,E)
+  let ltop = LevelLe 5
   let lseq = 4
   let ltactical = 3
   let lorelse = 2
@@ -645,13 +644,13 @@ let pr_goal_selector ~toplevel s =
   let ltatom = 1
   let linfo = 5
 
-  let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq
+  let level_of p = match p with LevelLe n -> n | LevelLt n -> n-1 | LevelSome -> lseq
 
   (** A printer for tactics that polymorphically works on the three
       "raw", "glob" and "typed" levels *)
 
   type 'a printer = {
-    pr_tactic    : tolerability -> 'tacexpr -> Pp.t;
+    pr_tactic    : entry_relative_level -> 'tacexpr -> Pp.t;
     pr_constr    : Environ.env -> Evd.evar_map -> 'trm -> Pp.t;
     pr_lconstr   : Environ.env -> Evd.evar_map -> 'trm -> Pp.t;
     pr_dconstr   : Environ.env -> Evd.evar_map -> 'dtrm -> Pp.t;
@@ -780,7 +779,7 @@ let pr_goal_selector ~toplevel s =
           hov 1 (
             primitive (if b then if ev then "eassert" else "assert" else if ev then "eenough" else "enough") ++
               pr_assumption (pr.pr_constr env sigma) (pr.pr_dconstr env sigma) (pr.pr_lconstr env sigma) ipat c ++
-              pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac
+              pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (LevelLe ltactical))) tac
           )
         | TacAssert (ev,_,None,ipat,c) ->
           hov 1 (
@@ -857,7 +856,7 @@ let pr_goal_selector ~toplevel s =
                   pr_with_bindings_arg_full (pr.pr_dconstr env sigma) (pr.pr_dconstr env sigma) c)
               l
             ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) cl
-            ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac
+            ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (LevelLe ltactical))) tac
           )
         | TacInversion (DepInversion (k,c,ids),hyp) ->
           hov 1 (
@@ -893,11 +892,11 @@ let pr_goal_selector ~toplevel s =
           let return (doc, l) = (tag tac doc, l) in
           let (strm, prec) = return (match tac with
             | TacAbstract (t,None) ->
-              keyword "abstract " ++ pr_tac (labstract,L) t, labstract
+              keyword "abstract " ++ pr_tac (LevelLt labstract) t, labstract
             | TacAbstract (t,Some s) ->
               hov 0 (
                 keyword "abstract"
-                ++ str" (" ++ pr_tac (labstract,L) t ++ str")" ++ spc ()
+                ++ str" (" ++ pr_tac (LevelLt labstract) t ++ str")" ++ spc ()
                 ++ keyword "using" ++ spc () ++ pr_id s),
               labstract
             | TacLetIn (recflag,llc,u) ->
@@ -906,7 +905,7 @@ let pr_goal_selector ~toplevel s =
                 (hv 0 (
                   pr_let_clauses recflag (pr.pr_generic env sigma) (pr_tac ltop) llc
                   ++ spc () ++ keyword "in"
-                 ) ++ fnl () ++ pr_tac (llet,E) u),
+                 ) ++ fnl () ++ pr_tac (LevelLe llet) u),
               llet
             | TacMatch (lz,t,lrul) ->
               hov 0 (
@@ -931,17 +930,17 @@ let pr_goal_selector ~toplevel s =
               hov 2 (
                 keyword "fun"
                 ++ prlist pr_funvar lvar ++ str " =>" ++ spc ()
-                ++ pr_tac (lfun,E) body),
+                ++ pr_tac (LevelLe lfun) body),
               lfun
             | TacThens (t,tl) ->
               hov 1 (
-                pr_tac (lseq,E) t ++ pr_then () ++ spc ()
+                pr_tac (LevelLe lseq) t ++ pr_then () ++ spc ()
                 ++ pr_seq_body (pr_opt_tactic (pr_tac ltop)) tl),
               lseq
             | TacThen (t1,t2) ->
               hov 1 (
-                pr_tac (lseq,E) t1 ++ pr_then () ++ spc ()
-                ++ pr_tac (lseq,L) t2),
+                pr_tac (LevelLe lseq) t1 ++ pr_then () ++ spc ()
+                ++ pr_tac (LevelLt lseq) t2),
               lseq
             | TacDispatch tl ->
               pr_dispatch (pr_tac ltop) tl, lseq
@@ -949,78 +948,78 @@ let pr_goal_selector ~toplevel s =
               pr_tac_extend (pr_tac ltop) tf t tr , lseq
             | TacThens3parts (t1,tf,t2,tl) ->
               hov 1 (
-                pr_tac (lseq,E) t1 ++ pr_then () ++ spc ()
+                pr_tac (LevelLe lseq) t1 ++ pr_then () ++ spc ()
                 ++ pr_then_gen (pr_tac ltop) tf t2 tl),
               lseq
             | TacTry t ->
               hov 1 (
-                keyword "try" ++ spc () ++ pr_tac (ltactical,E) t),
+                keyword "try" ++ spc () ++ pr_tac (LevelLe ltactical) t),
               ltactical
             | TacDo (n,t) ->
               hov 1 (
                 str "do" ++ spc ()
                 ++ pr_or_var int n ++ spc ()
-                ++ pr_tac (ltactical,E) t),
+                ++ pr_tac (LevelLe ltactical) t),
               ltactical
             | TacTimeout (n,t) ->
               hov 1 (
                 keyword "timeout "
                 ++ pr_or_var int n ++ spc ()
-                ++ pr_tac (ltactical,E) t),
+                ++ pr_tac (LevelLe ltactical) t),
               ltactical
             | TacTime (s,t) ->
               hov 1 (
                 keyword "time"
                 ++ pr_opt qstring s ++ spc ()
-                ++ pr_tac (ltactical,E) t),
+                ++ pr_tac (LevelLe ltactical) t),
               ltactical
             | TacRepeat t ->
               hov 1 (
                 keyword "repeat" ++ spc ()
-                ++ pr_tac (ltactical,E) t),
+                ++ pr_tac (LevelLe ltactical) t),
               ltactical
             | TacProgress t ->
               hov 1 (
                 keyword "progress" ++ spc ()
-                ++ pr_tac (ltactical,E) t),
+                ++ pr_tac (LevelLe ltactical) t),
               ltactical
             | TacShowHyps t ->
               hov 1 (
                 keyword "infoH" ++ spc ()
-                ++ pr_tac (ltactical,E) t),
+                ++ pr_tac (LevelLe ltactical) t),
               ltactical
             | TacInfo t ->
               hov 1 (
                 keyword "info" ++ spc ()
-                ++ pr_tac (ltactical,E) t),
+                ++ pr_tac (LevelLe ltactical) t),
               linfo
             | TacOr (t1,t2) ->
               hov 1 (
-                pr_tac (lorelse,L) t1 ++ spc ()
+                pr_tac (LevelLt lorelse) t1 ++ spc ()
                 ++ str "+" ++ brk (1,1)
-                ++ pr_tac (lorelse,E) t2),
+                ++ pr_tac (LevelLe lorelse) t2),
               lorelse
             | TacOnce t ->
               hov 1 (
                 keyword "once" ++ spc ()
-                ++ pr_tac (ltactical,E) t),
+                ++ pr_tac (LevelLe ltactical) t),
               ltactical
             | TacExactlyOnce t ->
               hov 1 (
                 keyword "exactly_once" ++ spc ()
-                ++ pr_tac (ltactical,E) t),
+                ++ pr_tac (LevelLe ltactical) t),
               ltactical
             | TacIfThenCatch (t,tt,te) ->
                 hov 1 (
-                 str"tryif" ++ spc() ++ pr_tac (ltactical,E) t ++ brk(1,1) ++
-                 str"then" ++ spc() ++ pr_tac (ltactical,E) tt ++ brk(1,1) ++
-                 str"else" ++ spc() ++ pr_tac (ltactical,E) te ++ brk(1,1)),
+                 str"tryif" ++ spc() ++ pr_tac (LevelLe ltactical) t ++ brk(1,1) ++
+                 str"then" ++ spc() ++ pr_tac (LevelLe ltactical) tt ++ brk(1,1) ++
+                 str"else" ++ spc() ++ pr_tac (LevelLe ltactical) te ++ brk(1,1)),
                 ltactical
             | TacOrelse (t1,t2) ->
               hov 1 (
-                pr_tac (lorelse,L) t1 ++ spc ()
+                pr_tac (LevelLt lorelse) t1 ++ spc ()
                 ++ str "||" ++ brk (1,1)
-                ++ pr_tac (lorelse,E) t2),
+                ++ pr_tac (LevelLe lorelse) t2),
               lorelse
             | TacFail (g,n,l) ->
               let arg =
@@ -1042,7 +1041,7 @@ let pr_goal_selector ~toplevel s =
             | TacSolve tl ->
               keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
             | TacComplete t ->
-              pr_tac (lcomplete,E) t, lcomplete
+              pr_tac (LevelLe lcomplete) t, lcomplete
             | TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, latom
             | TacId l ->
               keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
@@ -1398,10 +1397,10 @@ let () =
 let () =
   let printer env sigma _ _ prtac = prtac env sigma in
   declare_extra_genarg_pprule_with_level wit_tactic printer printer printer
-  ltop (0,E)
+  ltop (LevelLe 0)
 
 let () =
   let pr_unit _env _sigma _ _ _ _ () = str "()" in
   let printer env sigma _ _ prtac = prtac env sigma in
   declare_extra_genarg_pprule_with_level wit_ltac printer printer pr_unit
-  ltop (0,E)
+  ltop (LevelLe 0)
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 9cff3ea1eb..33db933168 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -16,7 +16,6 @@ open Geninterp
 open Names
 open Environ
 open Constrexpr
-open Notation_gram
 open Genintern
 open Tacexpr
 open Tactypes
@@ -29,43 +28,43 @@ type 'a raw_extra_genarg_printer =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) ->
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) ->
   'a -> Pp.t
 
 type 'a glob_extra_genarg_printer =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) ->
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) ->
   'a -> Pp.t
 
 type 'a extra_genarg_printer =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) ->
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) ->
   'a -> Pp.t
 
 type 'a raw_extra_genarg_printer_with_level =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) ->
-  tolerability -> 'a -> Pp.t
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) ->
+  entry_relative_level -> 'a -> Pp.t
 
 type 'a glob_extra_genarg_printer_with_level =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) ->
-  tolerability -> 'a -> Pp.t
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) ->
+  entry_relative_level -> 'a -> Pp.t
 
 type 'a extra_genarg_printer_with_level =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) ->
-  tolerability -> 'a -> Pp.t
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) ->
+  entry_relative_level -> 'a -> Pp.t
 
 val declare_extra_genarg_pprule :
   ('a, 'b, 'c) genarg_type ->
@@ -78,7 +77,7 @@ val declare_extra_genarg_pprule_with_level :
   'a raw_extra_genarg_printer_with_level ->
   'b glob_extra_genarg_printer_with_level ->
   'c extra_genarg_printer_with_level ->
-  (* surroounded *) tolerability -> (* non-surroounded *) tolerability -> unit
+  (* surroounded *) entry_relative_level -> (* non-surroounded *) entry_relative_level -> unit
 
 val declare_extra_vernac_genarg_pprule :
   ('a, 'b, 'c) genarg_type ->
@@ -140,7 +139,7 @@ val pr_ltac_constant : ltac_constant -> Pp.t
 
 val pr_raw_tactic : env -> Evd.evar_map -> raw_tactic_expr -> Pp.t
 
-val pr_raw_tactic_level : env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t
+val pr_raw_tactic_level : env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t
 
 val pr_glob_tactic : env -> glob_tactic_expr -> Pp.t
 
@@ -155,10 +154,10 @@ val pr_match_pattern : ('a -> Pp.t) -> 'a match_pattern -> Pp.t
 val pr_match_rule : bool -> ('a -> Pp.t) -> ('b -> Pp.t) ->
   ('b, 'a) match_rule -> Pp.t
 
-val pr_value : tolerability -> Val.t -> Pp.t
+val pr_value : entry_relative_level -> Val.t -> Pp.t
 
 
-val ltop : tolerability
+val ltop : entry_relative_level
 
-val make_constr_printer : (env -> Evd.evar_map -> tolerability -> 'a -> Pp.t) ->
+val make_constr_printer : (env -> Evd.evar_map -> entry_relative_level -> 'a -> Pp.t) ->
   'a Genprint.top_printer
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 21b832a326..3f67d55e73 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -90,7 +90,7 @@ let cast_arg wit v = Taccoerce.Value.cast (Genarg.topwit wit) v
  * we thus save the lexer to restore it at the end of the file *)
 let frozen_lexer = CLexer.get_keyword_state () ;;
 
-let tacltop = (5,Notation_gram.E)
+let tacltop = (LevelLe 5)
 
 let pr_ssrtacarg env sigma _ _ prt = prt env sigma tacltop
 
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index e6b1706b41..53c895f9d9 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -15,12 +15,12 @@ open Ltac_plugin
 val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t
 val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
 val pr_ssrtacarg : Environ.env -> Evd.evar_map -> 'a -> 'b ->
-  (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> 'c) -> 'c
+  (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> 'c) -> 'c
 
 val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t
 val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
 val pr_ssrtclarg : Environ.env -> Evd.evar_map -> 'a -> 'b ->
-  (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd
+  (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> 'c -> 'd) -> 'c -> 'd
 
 val add_genarg : string -> (Environ.env -> Evd.evar_map -> 'a -> Pp.t) -> 'a Genarg.uniform_genarg_type
 
diff --git a/printing/genprint.ml b/printing/genprint.ml
index a04df31d30..a673cbd933 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -19,15 +19,15 @@ open Geninterp
 (* Printing generic values *)
 
 type 'a with_level =
-  { default_already_surrounded : Notation_gram.tolerability;
-    default_ensure_surrounded : Notation_gram.tolerability;
+  { default_already_surrounded : Constrexpr.entry_relative_level;
+    default_ensure_surrounded : Constrexpr.entry_relative_level;
     printer : 'a }
 
 type printer_result =
 | PrinterBasic of (Environ.env -> Evd.evar_map -> Pp.t)
-| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t) with_level
+| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t) with_level
 
-type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t
+type printer_fun_with_level = Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t
 
 type top_printer_result =
 | TopPrinterBasic of (unit -> Pp.t)
diff --git a/printing/genprint.mli b/printing/genprint.mli
index 21b8417ffa..59e36baeb6 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -13,15 +13,15 @@
 open Genarg
 
 type 'a with_level =
-  { default_already_surrounded : Notation_gram.tolerability;
-    default_ensure_surrounded : Notation_gram.tolerability;
+  { default_already_surrounded : Constrexpr.entry_relative_level;
+    default_ensure_surrounded : Constrexpr.entry_relative_level;
     printer : 'a }
 
 type printer_result =
 | PrinterBasic of (Environ.env -> Evd.evar_map -> Pp.t)
-| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t) with_level
+| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t) with_level
 
-type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t
+type printer_fun_with_level = Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t
 
 type top_printer_result =
 | TopPrinterBasic of (unit -> Pp.t)
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 2f60663c82..c2d760ae08 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -20,7 +20,6 @@ open Ppextend
 open Glob_term
 open Constrexpr
 open Constrexpr_ops
-open Notation_gram
 open Namegen
 (*i*)
 
@@ -66,21 +65,16 @@ let tag_var = tag Tag.variable
   let lapp = 10
   let lposint = 0
   let lnegint = 35 (* must be consistent with Notation "- x" *)
-  let ltop = (200,E)
+  let ltop = LevelLe 200
   let lproj = 1
   let ldelim = 1
-  let lsimpleconstr = (8,E)
-  let lsimplepatt = (1,E)
-
-  let prec_less child (parent,assoc) =
-    if parent < 0 && Int.equal child lprod then true
-    else
-      let parent = abs parent in
-      match assoc with
-        | E -> (<=) child parent
-        | L -> (<) child parent
-        | Prec n -> child<=n
-        | Any -> true
+  let lsimpleconstr = LevelLe 8
+  let lsimplepatt = LevelLe 1
+
+  let prec_less child = function
+    | LevelLt parent -> (<) child parent
+    | LevelLe parent -> if parent < 0 && Int.equal child lprod then true else child <= abs parent
+    | LevelSome -> true
 
   let prec_of_prim_token = function
     | Numeral (SPlus,_) -> lposint
@@ -98,22 +92,22 @@ let tag_var = tag Tag.variable
     let rec aux = function
       | [] ->
         mt ()
-      | UnpMetaVar (_, prec) as unp :: l ->
+      | UnpMetaVar prec as unp :: l ->
         let c = pop env in
         let pp2 = aux l in
-        let pp1 = pr (n, prec) c in
+        let pp1 = pr prec c in
         return unp pp1 pp2
-      | UnpBinderMetaVar (_, prec) as unp :: l ->
+      | UnpBinderMetaVar prec as unp :: l ->
         let c = pop bl in
         let pp2 = aux l in
-        let pp1 = pr_patt (n, prec) c in
+        let pp1 = pr_patt prec c in
         return unp pp1 pp2
-      | UnpListMetaVar (_, prec, sl) as unp :: l ->
+      | UnpListMetaVar (prec, sl) as unp :: l ->
         let cl = pop envlist in
-        let pp1 = prlist_with_sep (fun () -> aux sl) (pr (n,prec)) cl in
+        let pp1 = prlist_with_sep (fun () -> aux sl) (pr prec) cl in
         let pp2 = aux l in
         return unp pp1 pp2
-      | UnpBinderListMetaVar (_, isopen, sl) as unp :: l ->
+      | UnpBinderListMetaVar (isopen, sl) as unp :: l ->
         let cl = pop bll in
         let pp2 = aux l in
         let pp1 = pr_binders (fun () -> aux sl) isopen cl in
@@ -216,7 +210,7 @@ let tag_var = tag Tag.variable
 
   let pr_expl_args pr (a,expl) =
     match expl with
-      | None -> pr (lapp,L) a
+      | None -> pr (LevelLt lapp) a
       | Some {v=ExplByPos (n,_id)} ->
         anomaly (Pp.str "Explicitation by position not implemented.")
       | Some {v=ExplByName id} ->
@@ -243,31 +237,32 @@ let tag_var = tag Tag.variable
   let las = lapp
   let lpator = 0
   let lpatrec = 0
+  let lpattop = LevelLe 200
 
   let rec pr_patt sep inh p =
     let (strm,prec) = match CAst.(p.v) with
       | CPatRecord l ->
         let pp (c, p) =
-          pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc (lpatrec, Any) p
+          pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc lpattop p
         in
         (if l = [] then str "{| |}"
          else str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}"), lpatrec
 
       | CPatAlias (p, na) ->
-        pr_patt mt (las,E) p ++ str " as " ++ pr_lname na, las
+        pr_patt mt (LevelLe las) p ++ str " as " ++ pr_lname na, las
 
       | CPatCstr (c, None, []) ->
         pr_reference c, latom
 
       | CPatCstr (c, None, args) ->
-        pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
+        pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) args, lapp
 
       | CPatCstr (c, Some args, []) ->
-        str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
+        str "@" ++ pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) args, lapp
 
       | CPatCstr (c, Some expl_args, extra_args) ->
-        surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) expl_args)
-        ++ prlist (pr_patt spc (lapp,L)) extra_args, lapp
+        surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) expl_args)
+        ++ prlist (pr_patt spc (LevelLt lapp)) extra_args, lapp
 
       | CPatAtom (None) ->
         str "_", latom
@@ -276,16 +271,16 @@ let tag_var = tag Tag.variable
         pr_reference r, latom
 
       | CPatOr pl ->
-        let pp p = hov 0 (pr_patt mt (lpator,Any) p) in
+        let pp p = hov 0 (pr_patt mt lpattop p) in
         surround (hov 0 (prlist_with_sep pr_spcbar pp pl)), lpator
 
       | CPatNotation (_,(_,"( _ )"),([p],[]),[]) ->
-        pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
+        pr_patt (fun()->str"(") lpattop p ++ str")", latom
 
       | CPatNotation (which,s,(l,ll),args) ->
         let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ -> mt ()) (fun _ _ _ -> mt()) which s (l,ll,[],[]) in
-        (if List.is_empty args||prec_less l_not (lapp,L) then strm_not else surround strm_not)
-        ++ prlist (pr_patt spc (lapp,L)) args, if not (List.is_empty args) then lapp else l_not
+        (if List.is_empty args||prec_less l_not (LevelLt lapp) then strm_not else surround strm_not)
+        ++ prlist (pr_patt spc (LevelLt lapp)) args, if not (List.is_empty args) then lapp else l_not
 
       | CPatPrim p ->
         pr_prim_token p, latom
@@ -440,7 +435,7 @@ let tag_var = tag Tag.variable
         | Some t -> spc () ++ keyword "in" ++ spc () ++ pr_patt lsimplepatt t)
 
   let pr_case_item pr (tm,as_clause, in_clause) =
-    hov 0 (pr (lcast,E) tm ++ pr_asin pr as_clause in_clause)
+    hov 0 (pr (LevelLe lcast) tm ++ pr_asin pr as_clause in_clause)
 
   let pr_case_type pr po =
     match po with
@@ -456,17 +451,17 @@ let tag_var = tag Tag.variable
       pr_case_type pr po
 
   let pr_proj pr pr_app a f l =
-    hov 0 (pr (lproj,E) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")")
+    hov 0 (pr (LevelLe lproj) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")")
 
   let pr_appexpl pr (f,us) l =
     hov 2 (
       str "@" ++ pr_reference f ++
         pr_universe_instance us ++
-        prlist (pr_sep_com spc (pr (lapp,L))) l)
+        prlist (pr_sep_com spc (pr (LevelLt lapp))) l)
 
   let pr_app pr a l =
     hov 2 (
-      pr (lapp,L) a  ++
+      pr (LevelLt lapp) a  ++
         prlist (fun a -> spc () ++ pr_expl_args pr a) l)
 
   let pr_record_body_gen pr l =
@@ -483,7 +478,7 @@ let tag_var = tag Tag.variable
   let pr_dangling_with_for sep pr inherited a =
     match a.v with
       | (CFix (_,[_])|CCoFix(_,[_])) ->
-        pr sep (latom,E) a
+        pr sep (LevelLe latom) a
       | _ ->
         pr sep inherited a
 
@@ -546,14 +541,14 @@ let tag_var = tag Tag.variable
         let c,l1 = List.sep_last l1 in
         let p = pr_proj (pr mt) pr_appexpl c (f,us) l1 in
         if not (List.is_empty l2) then
-          return (p ++ prlist (pr spc (lapp,L)) l2, lapp)
+          return (p ++ prlist (pr spc (LevelLt lapp)) l2, lapp)
         else
           return (p, lproj)
       | CAppExpl ((None,qid,us),[t])
       | CApp ((_, {v = CRef(qid,us)}),[t,None])
           when qualid_is_ident qid && Id.equal (qualid_basename qid) Notation_ops.ldots_var ->
         return (
-          hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."),
+          hov 0 (str ".." ++ pr spc (LevelLe latom) t ++ spc () ++ str ".."),
           larg
         )
       | CAppExpl ((None,f,us),l) ->
@@ -642,16 +637,16 @@ let tag_var = tag Tag.variable
         return (pr_glob_sort s, latom)
       | CCast (a,b) ->
         return (
-          hv 0 (pr mt (lcast,L) a ++ spc () ++
+          hv 0 (pr mt (LevelLt lcast) a ++ spc () ++
                   match b with
-                    | CastConv b -> str ":" ++ ws 1 ++ pr mt (-lcast,E) b
-                    | CastVM b -> str "<:" ++ ws 1 ++ pr mt (-lcast,E) b
-                    | CastNative b -> str "<<:" ++ ws 1 ++ pr mt (-lcast,E) b
+                    | CastConv b -> str ":" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b
+                    | CastVM b -> str "<:" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b
+                    | CastNative b -> str "<<:" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b
                     | CastCoerce -> str ":>"),
           lcast
         )
       | CNotation (_,(_,"( _ )"),([t],[],[],[])) ->
-        return (pr (fun()->str"(") (max_int,L) t ++ str")", latom)
+        return (pr (fun()->str"(") ltop t ++ str")", latom)
       | CNotation (which,s,env) ->
         pr_notation (pr mt) pr_patt (pr_binders_gen (pr mt ltop)) which s env
       | CGeneralization (bk,ak,c) ->
@@ -659,7 +654,7 @@ let tag_var = tag Tag.variable
       | CPrim p ->
         return (pr_prim_token p, prec_of_prim_token p)
       | CDelimiters (sc,a) ->
-        return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim)
+        return (pr_delimiters sc (pr mt (LevelLe ldelim) a), ldelim)
     in
     let loc = constr_loc a in
     pr_with_comments ?loc
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index c17ca251a8..288fb251c4 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -15,9 +15,8 @@
 open Libnames
 open Constrexpr
 open Names
-open Notation_gram
 
-val prec_less : precedence -> tolerability -> bool
+val prec_less : entry_level -> entry_relative_level -> bool
 
 val pr_tight_coma : unit -> Pp.t
 
@@ -49,7 +48,7 @@ val pr_lconstr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr
 val pr_constr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t
 val pr_lconstr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t
 val pr_cases_pattern_expr : cases_pattern_expr -> Pp.t
-val pr_constr_expr_n : Environ.env -> Evd.evar_map -> tolerability -> constr_expr -> Pp.t
+val pr_constr_expr_n : Environ.env -> Evd.evar_map -> entry_relative_level -> constr_expr -> Pp.t
 
 type term_pr = {
   pr_constr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t;
@@ -76,8 +75,8 @@ val default_term_pr : term_pr
   Which has the same type. We can turn a modular printer into a printer by
   taking its fixpoint. *)
 
-val lsimpleconstr : tolerability
-val ltop : tolerability
+val lsimpleconstr : entry_relative_level
+val ltop : entry_relative_level
 val modular_constr_pr :
-  ((unit->Pp.t) -> tolerability -> constr_expr -> Pp.t) ->
-  (unit->Pp.t) -> tolerability -> constr_expr -> Pp.t
+  ((unit->Pp.t) -> entry_relative_level -> constr_expr -> Pp.t) ->
+  (unit->Pp.t) -> entry_relative_level -> constr_expr -> Pp.t
diff --git a/printing/printer.mli b/printing/printer.mli
index cd5151bd8f..24d0a8cf6a 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -51,7 +51,7 @@ val enable_goal_names_printing     : bool ref
 val pr_constr_env          : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> constr -> Pp.t
 val pr_lconstr_env         : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> constr -> Pp.t
 
-val pr_constr_n_env        : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t
+val pr_constr_n_env        : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> constr -> Pp.t
 
 (** Same, but resilient to [Nametab] errors. Prints fully-qualified
     names when [shortest_qualid_of_global] has failed. Prints "??"
@@ -63,7 +63,7 @@ val safe_pr_lconstr_env : env -> evar_map -> constr -> Pp.t
 val pr_econstr_env      : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> EConstr.t -> Pp.t
 val pr_leconstr_env     : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> EConstr.t -> Pp.t
 
-val pr_econstr_n_env    : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t
+val pr_econstr_n_env    : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> EConstr.t -> Pp.t
 
 val pr_etype_env        : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t
 val pr_letype_env       : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t
@@ -100,7 +100,7 @@ val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp
 val pr_ltype_env           : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t
 val pr_type_env            : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t
 
-val pr_closed_glob_n_env   : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t
+val pr_closed_glob_n_env   : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> closed_glob_constr -> Pp.t
 val pr_closed_glob_env     : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> closed_glob_constr -> Pp.t
 
 val pr_ljudge_env          : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index aa439fae12..b26e725d9b 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -172,3 +172,16 @@ Notation "#" := 0 (only printing).
 Print Visibility.
 
 End Bug10750.
+
+Module M18.
+
+  Module A.
+    Module B.
+    Infix "+++" := Nat.add (at level 70).
+    End B.
+  End A.
+Import A.
+(* Check that the notation in module B is not visible *)
+Infix "+++" := Nat.add (at level 80).
+
+End M18.
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index b0b8a7612e..afff0347f5 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -286,32 +286,30 @@ let pr_notation_entry = function
   | InConstrEntry -> str "constr"
   | InCustomEntry s -> str "custom " ++ str s
 
-let prec_assoc = let open Gramlib.Gramext in function
-  | RightA -> (L,E)
-  | LeftA -> (E,L)
-  | NonA -> (L,L)
-
 let precedence_of_position_and_level from_level = function
-  | NumLevel n, BorderProd (_,None) -> n, Prec n
   | NumLevel n, BorderProd (b,Some a) ->
-      n, let (lp,rp) = prec_assoc a in if b == Left then lp else rp
-  | NumLevel n, InternalProd -> n, Prec n
-  | NextLevel, _ -> from_level, L
-  | DefaultLevel, _ ->
-      (* Fake value, waiting for PR#5 at herbelin's fork *) 200,
-      Any
+    (let open Gramlib.Gramext in
+     match a, b with
+     | RightA, Left -> LevelLt n
+     | RightA, Right -> LevelLe n
+     | LeftA, Left -> LevelLe n
+     | LeftA, Right -> LevelLt n
+     | NonA, _ -> LevelLt n)
+  | NumLevel n, _ -> LevelLe n
+  | NextLevel, _ -> LevelLt from_level
+  | DefaultLevel, _ -> LevelSome
 
 (** Computing precedences of subentries for parsing *)
 let precedence_of_entry_type (from_custom,from_level) = function
   | ETConstr (custom,_,x) when notation_entry_eq custom from_custom ->
     precedence_of_position_and_level from_level x
-  | ETConstr (custom,_,(NumLevel n,_)) -> n, Prec n
+  | ETConstr (custom,_,(NumLevel n,_)) -> LevelLe n
   | ETConstr (custom,_,(NextLevel,_)) ->
     user_err (strbrk "\"next level\" is only for sub-expressions in the same entry as where the notation is (" ++
               quote (pr_notation_entry custom) ++ strbrk " is different from " ++
               quote (pr_notation_entry from_custom) ++ str ").")
-  | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in n, Prec n
-  | _ -> 0, E (* should not matter *)
+  | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in LevelLe n
+  | _ -> LevelSome (* should not matter *)
 
 (** Computing precedences for future insertion of parentheses at
     the time of printing using hard-wired constr levels *)
@@ -320,14 +318,14 @@ let unparsing_precedence_of_entry_type from_level = function
     (* Possible insertion of parentheses at printing time to deal
        with precedence in a constr entry is managed using [prec_less]
        in [ppconstr.ml] *)
-    snd (precedence_of_position_and_level from_level x)
+    precedence_of_position_and_level from_level x
   | ETConstr (custom,_,_) ->
     (* Precedence of printing for a custom entry is managed using
        explicit insertion of entry coercions at the time of building
        a [constr_expr] *)
-    Any
-  | ETPattern (_,n) -> (* in constr *) Prec (match n with Some n -> n | None -> 0)
-  | _ -> Any (* should not matter *)
+    LevelSome
+  | ETPattern (_,n) -> (* in constr *) LevelLe (match n with Some n -> n | None -> 0)
+  | _ -> LevelSome (* should not matter *)
 
 (* Some breaking examples *)
 (* "x = y" : "x /1 = y" (breaks before any symbol) *)
@@ -397,11 +395,11 @@ let unparsing_metavar i from typs =
   let prec = unparsing_precedence_of_entry_type from x in
   match x with
   | ETConstr _ | ETGlobal | ETBigint ->
-     UnpMetaVar (i,prec)
+     UnpMetaVar prec
   | ETPattern _ ->
-     UnpBinderMetaVar (i,prec)
+     UnpBinderMetaVar prec
   | ETIdent ->
-     UnpBinderMetaVar (i,prec)
+     UnpBinderMetaVar prec
   | ETBinder isopen ->
      assert false
 
@@ -455,10 +453,10 @@ let make_hunks etyps symbols from_level =
           (* We add NonTerminal for simulation but remove it afterwards *)
           else make true sl in
         let hunk = match typ with
-          | ETConstr _ -> UnpListMetaVar (i,prec,List.map snd sl')
+          | ETConstr _ -> UnpListMetaVar (prec,List.map snd sl')
           | ETBinder isopen ->
               check_open_binder isopen sl m;
-              UnpBinderListMetaVar (i,isopen,List.map snd sl')
+              UnpBinderListMetaVar (isopen,List.map snd sl')
           | _ -> assert false in
         (None, hunk) :: make_with_space b prods
 
@@ -597,10 +595,10 @@ let hunks_of_format (from_level,(vars,typs)) symfmt =
       if not (List.is_empty sl) then error_format ?loc:(find_prod_list_loc loc_slfmt fmt) ();
       let symbs, l = aux (symbs,rfmt) in
       let hunk = match typ with
-        | ETConstr _ -> UnpListMetaVar (i,prec,slfmt)
+        | ETConstr _ -> UnpListMetaVar (prec,slfmt)
         | ETBinder isopen ->
             check_open_binder isopen sl m;
-            UnpBinderListMetaVar (i,isopen,slfmt)
+            UnpBinderListMetaVar (isopen,slfmt)
         | _ -> assert false in
       symbs, hunk :: l
   | symbs, (_,UnpBox (a,b)) :: fmt ->
@@ -745,15 +743,11 @@ let recompute_assoc typs = let open Gramlib.Gramext in
 
 let pr_arg_level from (lev,typ) =
   let pplev = function
-  | (n,L) when Int.equal n from -> str "at next level"
-  | (n,E) -> str "at level " ++ int n
-  | (n,L) -> str "at level below " ++ int n
-  | (n,Prec m) when Int.equal m n -> str "at level " ++ int n
-  | (n,_) -> str "Unknown level" in
-  Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++
-  (match typ with
-   | ETConstr _ | ETPattern _ -> spc () ++ pplev lev
-   | _ -> mt ())
+  | LevelLt n when Int.equal n from -> spc () ++ str "at next level"
+  | LevelLe n -> spc () ++ str "at level " ++ int n
+  | LevelLt n -> spc () ++ str "at level below " ++ int n
+  | LevelSome -> mt () in
+  Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++ pplev lev
 
 let pr_level ntn (from,fromlevel,args,typs) =
   (match from with InConstrEntry -> mt () | InCustomEntry s -> str "in " ++ str s ++ spc()) ++
@@ -1417,34 +1411,36 @@ let load_notation =
   load_notation_common true
 
 let open_notation i (_, nobj) =
-  let scope = nobj.notobj_scope in
-  let (ntn, df) = nobj.notobj_notation in
-  let pat = nobj.notobj_interp in
-  let onlyprint = nobj.notobj_onlyprint  in
-  let deprecation = nobj.notobj_deprecation in
-  let specific = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in
-  let specific_ntn = (specific,ntn) in
-  let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in
-  if Int.equal i 1 && fresh then begin
-    (* Declare the interpretation *)
-    let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in
-    (* Declare the uninterpretation *)
-    if not nobj.notobj_onlyparse then
-      Notation.declare_uninterpretation (NotationRule specific_ntn) pat;
-    (* Declare a possible coercion *)
-    (match nobj.notobj_coercion with
-    | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion specific_ntn entry
-    | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n
-    | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n
-    | None -> ())
-  end;
-  (* Declare specific format if any *)
-  match nobj.notobj_specific_pp_rules with
-  | Some pp_sy ->
-    if specific_format_to_declare specific_ntn pp_sy then
-      Ppextend.declare_specific_notation_printing_rules
-        specific_ntn ~extra:pp_sy.synext_extra pp_sy.synext_unparsing
-  | None -> ()
+  if Int.equal i 1 then begin
+    let scope = nobj.notobj_scope in
+    let (ntn, df) = nobj.notobj_notation in
+    let pat = nobj.notobj_interp in
+    let onlyprint = nobj.notobj_onlyprint  in
+    let deprecation = nobj.notobj_deprecation in
+    let specific = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in
+    let specific_ntn = (specific,ntn) in
+    let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in
+    if fresh then begin
+      (* Declare the interpretation *)
+      let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in
+      (* Declare the uninterpretation *)
+      if not nobj.notobj_onlyparse then
+        Notation.declare_uninterpretation (NotationRule specific_ntn) pat;
+      (* Declare a possible coercion *)
+      (match nobj.notobj_coercion with
+      | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion specific_ntn entry
+      | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n
+      | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n
+      | None -> ())
+      end;
+    (* Declare specific format if any *)
+    match nobj.notobj_specific_pp_rules with
+    | Some pp_sy ->
+      if specific_format_to_declare specific_ntn pp_sy then
+        Ppextend.declare_specific_notation_printing_rules
+          specific_ntn ~extra:pp_sy.synext_extra pp_sy.synext_unparsing
+    | None -> ()
+  end
 
 let cache_notation o =
   load_notation_common false 1 o;