Revert "Passing around the precedence to the generic printer so as to solve"

This reverts commit 8c74d3e5578caeb5c62ba462528d9972c1de17f1.

3 files changed, 9 insertions, 13 deletions

diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index e8dee7a00..e9c30e728 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1281,7 +1281,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       in
       let tac =
         Ftactic.with_env interp_vars >>= fun (env, lr) ->
-        let name () = Pptactic.pr_alias (fun _ v -> print_top_val env v) 0 s lr in
+        let name () = Pptactic.pr_alias (fun v -> print_top_val env v) 0 s lr in
         Proofview.Trace.name_tactic name (tac lr)
       (* spiwack: this use of name_tactic is not robust to a
          change of implementation of [Ftactic]. In such a situation,
@@ -1303,7 +1303,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       let tac = Tacenv.interp_ml_tactic opn in
       let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in
       let tac args =
-        let name () = Pptactic.pr_extend (fun _ v -> print_top_val () v) 0 opn args in
+        let name () = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in
         Proofview.Trace.name_tactic name (catch_error_tac trace (tac args ist))
       in
       Ftactic.run args tac
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 920f1d62a..a31b8b4da 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -345,13 +345,9 @@ module Make
 
   let rec tacarg_using_rule_token pr_gen = function
     | Egramml.GramTerminal s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al)
-    | Egramml.GramNonTerminal (_,Rawwit wit,e) :: l, a :: al ->
-      let lev = match e,wit with
-        | Extend.Aentryl (_,lev), ExtraArg t when ArgT.repr t = "tactic" -> lev
-        | Extend.Aentry _, ExtraArg t when ArgT.repr t = "tactic" -> 5
-        | _ -> 0 in
+    | Egramml.GramNonTerminal _ :: l, a :: al ->
       let r = tacarg_using_rule_token pr_gen (l,al) in
-      pr_gen (lev,E) a :: r
+      pr_gen a :: r
     | [], [] -> []
     | _ -> failwith "Inconsistent arguments of extended tactic"
 
@@ -376,7 +372,7 @@ module Make
       in
       let args = match l with
         | [] -> mt ()
-        | _ -> spc() ++ pr_sequence (pr_gen (1,Any)) l
+        | _ -> spc() ++ pr_sequence pr_gen l
       in
       str "<" ++ name ++ str ">" ++ args
 
@@ -388,13 +384,13 @@ module Make
       let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in
       if pp.pptac_level > lev then surround p else p
     with Not_found ->
-      KerName.print key ++ spc() ++ pr_sequence (pr_gen (1,Any)) l ++ str" (* Generic printer *)"
+      KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
 
   let check_type t arg = match arg with
   | TacGeneric arg -> argument_type_eq t (genarg_tag arg)
   | _ -> argument_type_eq t (ArgumentType wit_tactic)
 
-  let pr_farg prtac lev arg = prtac lev (TacArg (Loc.ghost, arg))
+  let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.ghost, arg))
 
   let pr_raw_extend_rec prc prlc prtac prpat =
     pr_extend_gen check_type (pr_farg prtac)
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index 0a8a22c3f..d4858bac4 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -44,9 +44,9 @@ module type Pp = sig
     ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds
 
   val pr_extend :
-    (tolerability -> Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds
+    (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds
 
-  val pr_alias : (tolerability -> Val.t -> std_ppcmds) ->
+  val pr_alias : (Val.t -> std_ppcmds) ->
     int -> Names.KerName.t -> Val.t list -> std_ppcmds
 
   val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds