Making structure of type "tolerability" and related clearer.

Also renamed it to relative_entry_level.

Correspondence between old and new representation is:
(n,L) -> LevelLt n
(n,E), (n,Prec n) -> LevelLe n
(n,Any) -> LevelSome
(n,Prec p) when n<>p was unused

Should not change global semantics (except error message in pr_arg).

5 files changed, 53 insertions, 59 deletions

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..75b3e7d406 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
@@ -101,16 +95,16 @@ let tag_var = tag Tag.variable
       | 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 ->
         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 ->
         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 ->
@@ -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