Merge PR #11635: Cleanup around the tolerability structure

Reviewed-by: ejgallego

6 files changed, 70 insertions, 72 deletions

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