Merge PR #9678: Stop accessing proof env via Pfedit in printers

Ack-by: JasonGross
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

10 files changed, 244 insertions, 228 deletions

diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index 5d5d45c58f..eb9cacb975 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -145,31 +145,30 @@ END
 
 let pr_occurrences = pr_occurrences () () ()
 
-let pr_gen prc _prlc _prtac c = prc c
+let pr_gen env sigma prc _prlc _prtac x = prc env sigma x
 
-let pr_globc _prc _prlc _prtac (_,glob) =
-  let _, env = Pfedit.get_current_context () in
+let pr_globc env sigma _prc _prlc _prtac (_,glob) =
   Printer.pr_glob_constr_env env glob
 
 let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t)
 
 let glob_glob = Tacintern.intern_constr
 
-let pr_lconstr _ prc _ c = prc c
+let pr_lconstr env sigma _ prc _ c = prc env sigma c
 
 let subst_glob = Tacsubst.subst_glob_constr_and_expr
 
 }
 
 ARGUMENT EXTEND glob
-    PRINTED BY { pr_globc }
+    PRINTED BY { pr_globc env sigma }
 
      INTERPRETED BY { interp_glob }
      GLOBALIZED BY { glob_glob }
      SUBSTITUTED BY { subst_glob }
 
-     RAW_PRINTED BY { pr_gen }
-     GLOB_PRINTED BY { pr_gen }
+     RAW_PRINTED BY { pr_gen env sigma }
+     GLOB_PRINTED BY { pr_gen env sigma }
 | [ constr(c) ] -> { c }
 END
 
@@ -181,20 +180,20 @@ let l_constr = Pcoq.Constr.lconstr
 
 ARGUMENT EXTEND lconstr
     TYPED AS constr
-    PRINTED BY { pr_lconstr }
+    PRINTED BY { pr_lconstr env sigma }
 | [ l_constr(c) ] -> { c }
 END
 
 ARGUMENT EXTEND lglob
   TYPED AS glob
-    PRINTED BY { pr_globc }
+    PRINTED BY { pr_globc env sigma }
 
      INTERPRETED BY { interp_glob }
      GLOBALIZED BY { glob_glob }
      SUBSTITUTED BY { subst_glob }
 
-     RAW_PRINTED BY { pr_gen }
-     GLOB_PRINTED BY { pr_gen }
+     RAW_PRINTED BY { pr_gen env sigma }
+     GLOB_PRINTED BY { pr_gen env sigma }
 | [ lconstr(c) ] -> { c }
 END
 
@@ -207,7 +206,7 @@ let interp_casted_constr ist gl c =
 
 ARGUMENT EXTEND casted_constr
   TYPED AS constr
-  PRINTED BY { pr_gen }
+  PRINTED BY { pr_gen env sigma }
   INTERPRETED BY { interp_casted_constr }
 | [ constr(c) ] -> { c }
 END
@@ -296,23 +295,23 @@ END
 
 {
 
-let pr_by_arg_tac _prc _prlc prtac opt_c =
+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 (3,Notation_gram.E) t)
+    | Some t -> hov 2 (str "by" ++ spc () ++ prtac env sigma (3,Notation_gram.E) t)
 
 }
 
 ARGUMENT EXTEND by_arg_tac
   TYPED AS tactic option
-  PRINTED BY { pr_by_arg_tac }
+  PRINTED BY { pr_by_arg_tac env sigma }
 | [ "by" tactic3(c) ] -> { Some c }
 | [ ] -> { None }
 END
 
 {
 
-let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c
+let pr_by_arg_tac env sigma prtac opt_c = pr_by_arg_tac env sigma () () prtac opt_c
 
 let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Pputils.pr_lident cl
 let pr_in_top_clause _ _ _ cl = Pptactic.pr_in_clause Id.print cl
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 0509d6ae71..7f9eecbef5 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -65,8 +65,9 @@ val wit_by_arg_tac :
   glob_tactic_expr option,
   Geninterp.Val.t option) Genarg.genarg_type
 
-val pr_by_arg_tac : 
-  (int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) ->
+val pr_by_arg_tac :
+  Environ.env -> Evd.evar_map ->
+  (Environ.env -> Evd.evar_map -> int * Notation_gram.parenRelation -> 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/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 663537f3e8..3a4b0571d4 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -62,21 +62,19 @@ let eval_uconstrs ist cs =
   let map c env sigma = c env sigma in
   List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs
 
-let pr_auto_using_raw _ _ _  = Pptactic.pr_auto_using Ppconstr.pr_constr_expr
-let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) ->
-    let _, env = Pfedit.get_current_context () in
+let pr_auto_using_raw env sigma _ _ _  = Pptactic.pr_auto_using @@ Ppconstr.pr_constr_expr env sigma
+let pr_auto_using_glob env sigma _ _ _ = Pptactic.pr_auto_using (fun (c,_) ->
     Printer.pr_glob_constr_env env c)
-let pr_auto_using _ _ _ = Pptactic.pr_auto_using
-    (let sigma, env = Pfedit.get_current_context () in
-     Printer.pr_closed_glob_env env sigma)
+let pr_auto_using env sigma _ _ _ = Pptactic.pr_auto_using @@
+     Printer.pr_closed_glob_env env sigma
 
 }
 
 ARGUMENT EXTEND auto_using
   TYPED AS uconstr list
-  PRINTED BY { pr_auto_using }
-  RAW_PRINTED BY { pr_auto_using_raw }
-  GLOB_PRINTED BY { pr_auto_using_glob }
+  PRINTED BY { pr_auto_using env sigma }
+  RAW_PRINTED BY { pr_auto_using_raw env sigma }
+  GLOB_PRINTED BY { pr_auto_using_glob env sigma }
 | [ "using" ne_uconstr_list_sep(l, ",") ] -> { l }
 | [ ] -> { [] }
 END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 4c24f51b1e..a348e2cea4 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -514,7 +514,7 @@ END
 
 let pr_ltac_ref = Libnames.pr_qualid
 
-let pr_tacdef_body tacdef_body =
+let pr_tacdef_body env sigma tacdef_body =
   let id, redef, body =
     match tacdef_body with
     | TacticDefinition ({CAst.v=id}, body) -> Id.print id, false, body
@@ -528,12 +528,12 @@ let pr_tacdef_body tacdef_body =
     prlist (function Name.Anonymous -> str " _"
       | Name.Name id -> spc () ++ Id.print id) idl
   ++ (if redef then str" ::=" else str" :=") ++ brk(1,1)
-  ++ Pptactic.pr_raw_tactic body
+  ++ Pptactic.pr_raw_tactic env sigma body
 
 }
 
 VERNAC ARGUMENT EXTEND ltac_tacdef_body
-PRINTED BY { pr_tacdef_body }
+PRINTED BY { pr_tacdef_body env sigma }
 | [ tacdef_body(t) ] -> { t }
 END
 
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index cdee012a82..a12dee48a8 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -162,9 +162,9 @@ END
 
 (* Declare a printer for the content of Program tactics *)
 let () =
-  let printer _ _ _ = function
+  let printer env sigma _ _ _ = function
   | None -> mt ()
-  | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac
+  | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic env sigma tac
   in
   Pptactic.declare_extra_vernac_genarg_pprule wit_withtac printer
 
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index db8d1b20d8..86a227415a 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -41,13 +41,11 @@ type constr_expr_with_bindings = constr_expr with_bindings
 type glob_constr_with_bindings = glob_constr_and_expr with_bindings
 type glob_constr_with_bindings_sign = interp_sign * glob_constr_and_expr with_bindings
 
-let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) =
-  let _, env = Pfedit.get_current_context () in
+let pr_glob_constr_with_bindings_sign env sigma _ _ _ (ge : glob_constr_with_bindings_sign) =
   Printer.pr_glob_constr_env env (fst (fst (snd ge)))
-let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) =
-  let _, env = Pfedit.get_current_context () in
+let pr_glob_constr_with_bindings env sigma _ _ _ (ge : glob_constr_with_bindings) =
   Printer.pr_glob_constr_env env (fst (fst ge))
-let pr_constr_expr_with_bindings prc _ _ (ge : constr_expr_with_bindings) = prc (fst ge)
+let pr_constr_expr_with_bindings env sigma prc _ _ (ge : constr_expr_with_bindings) = prc env sigma (fst ge)
 let interp_glob_constr_with_bindings ist gl c = Tacmach.project gl , (ist, c)
 let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings ist l
 let subst_glob_constr_with_bindings s c =
@@ -56,14 +54,14 @@ let subst_glob_constr_with_bindings s c =
 }
 
 ARGUMENT EXTEND glob_constr_with_bindings
-    PRINTED BY { pr_glob_constr_with_bindings_sign }
+    PRINTED BY { pr_glob_constr_with_bindings_sign env sigma }
 
     INTERPRETED BY { interp_glob_constr_with_bindings }
     GLOBALIZED BY { glob_glob_constr_with_bindings }
     SUBSTITUTED BY { subst_glob_constr_with_bindings }
 
-    RAW_PRINTED BY { pr_constr_expr_with_bindings }
-    GLOB_PRINTED BY { pr_glob_constr_with_bindings }
+    RAW_PRINTED BY { pr_constr_expr_with_bindings env sigma }
+    GLOB_PRINTED BY { pr_glob_constr_with_bindings env sigma }
 
 | [ constr_with_bindings(bl) ] -> { bl }
 END
@@ -80,17 +78,17 @@ let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (fun c -> c
 let subst_strategy s str = str
 
 let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>"
-let pr_raw_strategy prc prlc _ (s : raw_strategy) =
-  let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in
-  Rewrite.pr_strategy prc prr s
-let pr_glob_strategy prc prlc _ (s : glob_strategy) =
-  let prr = Pptactic.pr_red_expr
+let pr_raw_strategy env sigma prc prlc _ (s : raw_strategy) =
+  let prr = Pptactic.pr_red_expr env sigma (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in
+  Rewrite.pr_strategy (prc env sigma) prr s
+let pr_glob_strategy env sigma prc prlc _ (s : glob_strategy) =
+  let prr = Pptactic.pr_red_expr env sigma
     (Ppconstr.pr_constr_expr,
     Ppconstr.pr_lconstr_expr,
     Pputils.pr_or_by_notation Libnames.pr_qualid,
     Ppconstr.pr_constr_expr)
   in
-  Rewrite.pr_strategy prc prr s
+  Rewrite.pr_strategy (prc env sigma) prr s
 
 }
 
@@ -101,8 +99,8 @@ ARGUMENT EXTEND rewstrategy
     GLOBALIZED BY { glob_strategy }
     SUBSTITUTED BY { subst_strategy }
 
-    RAW_PRINTED BY { pr_raw_strategy }
-    GLOB_PRINTED BY { pr_glob_strategy }
+    RAW_PRINTED BY { pr_raw_strategy env sigma }
+    GLOB_PRINTED BY { pr_glob_strategy env sigma }
 
   | [ glob(c) ] -> { StratConstr (c, true) }
   | [ "<-" constr(c) ] -> { StratConstr (c, false) }
@@ -224,7 +222,7 @@ let wit_binders =
 let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wit_binders)
 
 let () =
-  let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in
+  let raw_printer env sigma _ _ _ l = Pp.pr_non_empty_arg (Ppconstr.pr_binders env sigma) l in
   Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer
 
 }
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index e188971f00..1bdba699f7 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -71,40 +71,46 @@ let declare_notation_tactic_pprule kn pt =
   prnotation_tab := KNmap.add kn pt !prnotation_tab
 
 type 'a raw_extra_genarg_printer =
-    (constr_expr -> Pp.t) ->
-    (constr_expr -> Pp.t) ->
-    (tolerability -> raw_tactic_expr -> Pp.t) ->
-    'a -> Pp.t
+  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) ->
+  'a -> Pp.t
 
 type 'a glob_extra_genarg_printer =
-    (glob_constr_and_expr -> Pp.t) ->
-    (glob_constr_and_expr -> Pp.t) ->
-    (tolerability -> glob_tactic_expr -> Pp.t) ->
-    'a -> Pp.t
+  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) ->
+  'a -> Pp.t
 
 type 'a extra_genarg_printer =
-    (EConstr.constr -> Pp.t) ->
-    (EConstr.constr -> Pp.t) ->
-    (tolerability -> Val.t -> Pp.t) ->
-    'a -> Pp.t
+  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) ->
+  'a -> Pp.t
 
 type 'a raw_extra_genarg_printer_with_level =
-    (constr_expr -> Pp.t) ->
-    (constr_expr -> Pp.t) ->
-    (tolerability -> raw_tactic_expr -> Pp.t) ->
-    tolerability -> 'a -> Pp.t
+  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
 
 type 'a glob_extra_genarg_printer_with_level =
-    (glob_constr_and_expr -> Pp.t) ->
-    (glob_constr_and_expr -> Pp.t) ->
-    (tolerability -> glob_tactic_expr -> Pp.t) ->
-    tolerability -> 'a -> Pp.t
+  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
 
 type 'a extra_genarg_printer_with_level =
-    (EConstr.constr -> Pp.t) ->
-    (EConstr.constr -> Pp.t) ->
-    (tolerability -> Val.t -> Pp.t) ->
-    tolerability -> 'a -> Pp.t
+  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
 
 let string_of_genarg_arg (ArgumentType arg) =
   let rec aux : type a b c. (a, b, c) genarg_type -> string = function
@@ -160,27 +166,27 @@ let string_of_genarg_arg (ArgumentType arg) =
         | _ -> default
 
   let pr_with_occurrences pr c = Ppred.pr_with_occurrences pr keyword c
-  let pr_red_expr pr c = Ppred.pr_red_expr pr keyword c
+  let pr_red_expr env sigma pr c = Ppred.pr_red_expr_env env sigma pr keyword c
 
-  let pr_may_eval test prc prlc pr2 pr3 = function
+  let pr_may_eval env sigma test prc prlc pr2 pr3 = function
     | ConstrEval (r,c) ->
       hov 0
         (keyword "eval" ++ brk (1,1) ++
-           pr_red_expr (prc,prlc,pr2,pr3) r ++ spc () ++
-           keyword "in" ++ spc() ++ prc c)
+           pr_red_expr env sigma (prc,prlc,pr2,pr3) r ++ spc () ++
+           keyword "in" ++ spc() ++ prc env sigma c)
     | ConstrContext ({CAst.v=id},c) ->
       hov 0
         (keyword "context" ++ spc () ++ pr_id id ++ spc () ++
-           str "[ " ++ prlc c ++ str " ]")
+           str "[ " ++ prlc env sigma c ++ str " ]")
     | ConstrTypeOf c ->
-      hov 1 (keyword "type of" ++ spc() ++ prc c)
+      hov 1 (keyword "type of" ++ spc() ++ prc env sigma c)
     | ConstrTerm c when test c ->
-      h 0 (str "(" ++ prc c ++ str ")")
+      h 0 (str "(" ++ prc env sigma c ++ str ")")
     | ConstrTerm c ->
-      prc c
+      prc env sigma c
 
-  let pr_may_eval a =
-    pr_may_eval (fun _ -> false) a
+  let pr_may_eval env sigma a =
+    pr_may_eval env sigma (fun _ -> false) a
 
   let pr_arg pr x = spc () ++ pr x
 
@@ -647,15 +653,15 @@ let pr_goal_selector ~toplevel s =
 
   type 'a printer = {
     pr_tactic    : tolerability -> 'tacexpr -> Pp.t;
-    pr_constr    : 'trm -> Pp.t;
-    pr_lconstr   : 'trm -> Pp.t;
-    pr_dconstr   : 'dtrm -> Pp.t;
-    pr_pattern   : 'pat -> Pp.t;
-    pr_lpattern  : 'pat -> 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;
+    pr_pattern   : Environ.env -> Evd.evar_map -> 'pat -> Pp.t;
+    pr_lpattern  : Environ.env -> Evd.evar_map -> 'pat -> Pp.t;
     pr_constant  : 'cst -> Pp.t;
     pr_reference : 'ref -> Pp.t;
     pr_name      : 'nam -> Pp.t;
-    pr_generic   : 'lev generic_argument -> Pp.t;
+    pr_generic   : Environ.env -> Evd.evar_map -> 'lev generic_argument -> Pp.t;
     pr_extend    : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> Pp.t;
     pr_alias     : int -> KerName.t -> 'a gen_tactic_arg list -> Pp.t;
   }
@@ -671,14 +677,14 @@ let pr_goal_selector ~toplevel s =
       level     :'lev
     >
 
-    let pr_atom pr strip_prod_binders tag_atom =
-      let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in
+    let pr_atom env sigma pr strip_prod_binders tag_atom =
+      let pr_with_bindings = pr_with_bindings (pr.pr_constr env sigma) (pr.pr_lconstr env sigma) in
       let pr_with_bindings_arg_full = pr_with_bindings_arg in
-      let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in
-      let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
+      let pr_with_bindings_arg = pr_with_bindings_arg (pr.pr_constr env sigma) (pr.pr_lconstr env sigma) in
+      let pr_red_expr = pr_red_expr env sigma (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
 
-      let _pr_constrarg c = spc () ++ pr.pr_constr c in
-      let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in
+      let _pr_constrarg c = spc () ++ pr.pr_constr env sigma c in
+      let pr_lconstrarg c = spc () ++ pr.pr_lconstr env sigma c in
       let pr_intarg n = spc () ++ int n in
 
       (* Some printing combinators *)
@@ -688,7 +694,7 @@ let pr_goal_selector ~toplevel s =
         (*  match t with
             | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
             | _ ->*)
-        let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in
+        let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr env sigma t in
         spc() ++ hov 1 (str"(" ++ s ++ str")") in
 
       let pr_fix_tac (id,n,c) =
@@ -723,7 +729,7 @@ let pr_goal_selector ~toplevel s =
         in
         hov 1 (str"(" ++ pr_id id ++
                   prlist pr_binder_fix bll ++ annot ++ str" :" ++
-                  pr_lconstrarg ty ++ str")") in
+                  (pr_lconstrarg ty) ++ str")") in
       (*  spc() ++
           hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ _pr_constrarg
           c)
@@ -747,13 +753,13 @@ let pr_goal_selector ~toplevel s =
            hov 1 (primitive (if ev then "eintros" else "intros") ++
                     (match p with
                     | [{CAst.v=IntroForthcoming false}] -> mt ()
-                    | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p))
+                    | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern @@ pr.pr_dconstr env sigma) p))
         | TacApply (a,ev,cb,inhyp) ->
           hov 1 (
             (if a then mt() else primitive "simple ") ++
               primitive (with_evars ev "apply") ++ spc () ++
               prlist_with_sep pr_comma pr_with_bindings_arg cb ++
-              pr_non_empty_arg (pr_in_hyp_as pr.pr_dconstr pr.pr_name) inhyp
+              pr_non_empty_arg (pr_in_hyp_as (pr.pr_dconstr env sigma) pr.pr_name) inhyp
           )
         | TacElim (ev,cb,cbo) ->
           hov 1 (
@@ -774,28 +780,28 @@ let pr_goal_selector ~toplevel s =
         | TacAssert (ev,b,Some tac,ipat,c) ->
           hov 1 (
             primitive (if b then if ev then "eassert" else "assert" else if ev then "eenough" else "enough") ++
-              pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++
+              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
           )
         | TacAssert (ev,_,None,ipat,c) ->
           hov 1 (
             primitive (if ev then "epose proof" else "pose proof")
-            ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c
+            ++ pr_assertion (pr.pr_constr env sigma) (pr.pr_dconstr env sigma) (pr.pr_lconstr env sigma) ipat c
           )
         | TacGeneralize l ->
           hov 1 (
             primitive "generalize" ++ spc ()
             ++ prlist_with_sep pr_comma (fun (cl,na) ->
-              pr_with_occurrences pr.pr_constr cl ++ pr_as_name na)
+              pr_with_occurrences (pr.pr_constr env sigma) cl ++ pr_as_name na)
               l
           )
         | TacLetTac (ev,na,c,cl,true,_) when Locusops.is_nowhere cl ->
-          hov 1 (primitive (if ev then "epose" else "pose") ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
+          hov 1 (primitive (if ev then "epose" else "pose") ++ pr_pose (pr.pr_constr env sigma) (pr.pr_lconstr env sigma) na c)
         | TacLetTac (ev,na,c,cl,b,e) ->
           hov 1 (
             primitive (if b then if ev then "eset" else "set" else if ev then "eremember" else "remember") ++
-              (if b then pr_pose pr.pr_constr pr.pr_lconstr na c
-                else pr_pose_as_style pr.pr_constr na c) ++
+              (if b then pr_pose (pr.pr_constr env sigma) (pr.pr_lconstr env sigma) na c
+                else pr_pose_as_style (pr.pr_constr env sigma) na c) ++
               pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++
               pr_non_empty_arg (pr_clauses (Some b) pr.pr_name) cl)
         (*  | TacInstantiate (n,c,ConclLocation ()) ->
@@ -815,8 +821,8 @@ let pr_goal_selector ~toplevel s =
             primitive (with_evars ev (if isrec then "induction" else "destruct"))
             ++ spc ()
             ++ prlist_with_sep pr_comma (fun (h,ids,cl) ->
-              pr_destruction_arg pr.pr_dconstr pr.pr_dconstr h ++
-                pr_non_empty_arg (pr_with_induction_names pr.pr_dconstr) ids ++
+              pr_destruction_arg (pr.pr_dconstr env sigma) (pr.pr_dconstr env sigma) h ++
+                pr_non_empty_arg (pr_with_induction_names (pr.pr_dconstr env sigma)) ids ++
                 pr_opt (pr_clauses None pr.pr_name) cl) l ++
               pr_opt pr_eliminator el
           )
@@ -835,9 +841,9 @@ let pr_goal_selector ~toplevel s =
                   None ->
                     mt ()
                 | Some p ->
-                  pr.pr_pattern p ++ spc ()
+                  pr.pr_pattern env sigma p ++ spc ()
                   ++ keyword "with" ++ spc ()
-            ) ++ pr.pr_dconstr c ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
+            ) ++ pr.pr_dconstr env sigma c ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
           )
 
         (* Equality and inversion *)
@@ -848,7 +854,7 @@ let pr_goal_selector ~toplevel s =
               (fun () -> str ","++spc())
               (fun (b,m,c) ->
                 pr_orient b ++ pr_multi m ++
-                  pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c)
+                  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
@@ -857,28 +863,28 @@ let pr_goal_selector ~toplevel s =
           hov 1 (
             primitive "dependent " ++ pr_inversion_kind k ++ spc ()
             ++ pr_quantified_hypothesis hyp
-            ++ pr_with_inversion_names pr.pr_dconstr ids
-            ++ pr_with_constr pr.pr_constr c
+            ++ pr_with_inversion_names (pr.pr_dconstr env sigma) ids
+            ++ pr_with_constr (pr.pr_constr env sigma) c
           )
         | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
           hov 1 (
             pr_inversion_kind k ++ spc ()
             ++ pr_quantified_hypothesis hyp
-            ++ pr_non_empty_arg (pr_with_inversion_names pr.pr_dconstr) ids
+            ++ pr_non_empty_arg (pr_with_inversion_names @@ pr.pr_dconstr env sigma) ids
             ++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl
           )
         | TacInversion (InversionUsing (c,cl),hyp) ->
           hov 1 (
             primitive "inversion" ++ spc()
             ++ pr_quantified_hypothesis hyp ++ spc ()
-            ++ keyword "using" ++ spc () ++ pr.pr_constr c
+            ++ keyword "using" ++ spc () ++ pr.pr_constr env sigma c
             ++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl
           )
       )
       in
       pr_atom1
 
-    let make_pr_tac pr strip_prod_binders tag_atom tag =
+    let make_pr_tac env sigma pr strip_prod_binders tag_atom tag =
 
         let extract_binders = function
           | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body)
@@ -898,7 +904,7 @@ let pr_goal_selector ~toplevel s =
               let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in
               v 0
                 (hv 0 (
-                  pr_let_clauses recflag pr.pr_generic (pr_tac ltop) llc
+                  pr_let_clauses recflag (pr.pr_generic env sigma) (pr_tac ltop) llc
                   ++ spc () ++ keyword "in"
                  ) ++ fnl () ++ pr_tac (llet,E) u),
               llet
@@ -908,7 +914,7 @@ let pr_goal_selector ~toplevel s =
                 ++ pr_tac ltop t ++ spc () ++ keyword "with"
                 ++ prlist (fun r ->
                   fnl () ++ str "| "
-                  ++ pr_match_rule true (pr_tac ltop) pr.pr_lpattern r
+                  ++ pr_match_rule true (pr_tac ltop) (pr.pr_lpattern env sigma) r
                 ) lrul
                 ++ fnl() ++ keyword "end"),
               lmatch
@@ -918,7 +924,7 @@ let pr_goal_selector ~toplevel s =
                 ++ keyword (if lr then "match reverse goal with" else "match goal with")
                 ++ prlist (fun r ->
                   fnl () ++ str "| "
-                  ++ pr_match_rule false (pr_tac ltop) pr.pr_lpattern r
+                  ++ pr_match_rule false (pr_tac ltop) (pr.pr_lpattern env sigma) r
                 ) lrul ++ fnl() ++ keyword "end"),
               lmatch
             | TacFun (lvar,body) ->
@@ -1041,17 +1047,17 @@ let pr_goal_selector ~toplevel s =
             | TacId l ->
               keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
             | TacAtom { CAst.loc; v=t } ->
-              pr_with_comments ?loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom
+              pr_with_comments ?loc (hov 1 (pr_atom env sigma pr strip_prod_binders tag_atom t)), ltatom
             | TacArg { CAst.v=Tacexp e } ->
               pr_tac inherited e, latom
             | TacArg { CAst.v=ConstrMayEval (ConstrTerm c) } ->
-              keyword "constr:" ++ pr.pr_constr c, latom
+              keyword "constr:" ++ pr.pr_constr env sigma c, latom
             | TacArg { CAst.v=ConstrMayEval c } ->
-              pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c, leval
+              pr_may_eval env sigma pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c, leval
             | TacArg { CAst.v=TacFreshId l } ->
               primitive "fresh" ++ pr_fresh_ids l, latom
             | TacArg { CAst.v=TacGeneric arg } ->
-              pr.pr_generic arg, latom
+              pr.pr_generic env sigma arg, latom
             | TacArg { CAst.v=TacCall {CAst.v=(f,[])} } ->
               pr.pr_reference f, latom
             | TacArg { CAst.v=TacCall {CAst.loc; v=(f,l)} } ->
@@ -1074,11 +1080,11 @@ let pr_goal_selector ~toplevel s =
           | Reference r ->
             pr.pr_reference r
           | ConstrMayEval c ->
-            pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c
+            pr_may_eval env sigma pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c
           | TacFreshId l ->
             keyword "fresh" ++ pr_fresh_ids l
           | TacPretype c ->
-            keyword "type_term" ++ pr.pr_constr c
+            keyword "type_term" ++ pr.pr_constr env sigma c
           | TacNumgoals ->
             keyword "numgoals"
           | (TacCall _|Tacexp _ | TacGeneric _) as a ->
@@ -1098,9 +1104,9 @@ let pr_goal_selector ~toplevel s =
   let raw_printers =
     (strip_prod_binders_expr)
 
-  let rec pr_raw_tactic_level n (t:raw_tactic_expr) =
+  let rec pr_raw_tactic_level env sigma n (t:raw_tactic_expr) =
     let pr = {
-      pr_tactic = pr_raw_tactic_level;
+      pr_tactic = pr_raw_tactic_level env sigma;
       pr_constr = pr_constr_expr;
       pr_dconstr = pr_constr_expr;
       pr_lconstr = pr_lconstr_expr;
@@ -1109,16 +1115,16 @@ let pr_goal_selector ~toplevel s =
       pr_constant = pr_or_by_notation pr_qualid;
       pr_reference = pr_qualid;
       pr_name = pr_lident;
-      pr_generic = (fun arg -> Pputils.pr_raw_generic (Global.env ()) arg);
-      pr_extend = pr_raw_extend_rec pr_raw_tactic_level;
-      pr_alias = pr_raw_alias pr_raw_tactic_level;
+      pr_generic = Pputils.pr_raw_generic;
+      pr_extend = pr_raw_extend_rec @@ pr_raw_tactic_level env sigma;
+      pr_alias = pr_raw_alias @@ pr_raw_tactic_level env sigma;
     } in
-    make_pr_tac
+    make_pr_tac env sigma
       pr raw_printers
       tag_raw_atomic_tactic_expr tag_raw_tactic_expr
       n t
 
-  let pr_raw_tactic = pr_raw_tactic_level ltop
+  let pr_raw_tactic env sigma = pr_raw_tactic_level env sigma ltop
 
   let pr_and_constr_expr pr (c,_) = pr c
 
@@ -1131,19 +1137,19 @@ let pr_goal_selector ~toplevel s =
     let rec prtac n (t:glob_tactic_expr) =
       let pr = {
         pr_tactic = prtac;
-        pr_constr = pr_and_constr_expr (pr_glob_constr_env env);
-        pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
-        pr_lconstr = pr_and_constr_expr (pr_lglob_constr_env env);
-        pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env);
-        pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env);
+        pr_constr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
+        pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
+        pr_lconstr = (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env));
+        pr_pattern = (fun env sigma -> pr_pat_and_constr_expr (pr_glob_constr_env env));
+        pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env));
         pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env));
         pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant);
         pr_name = pr_lident;
-        pr_generic = (fun arg -> Pputils.pr_glb_generic (Global.env ()) arg);
+        pr_generic = Pputils.pr_glb_generic;
         pr_extend = pr_glob_extend_rec prtac;
         pr_alias = pr_glob_alias prtac;
       } in
-      make_pr_tac
+      make_pr_tac env (Evd.from_env env)
         pr glob_printers
         tag_glob_atomic_tactic_expr tag_glob_tactic_expr
         n t
@@ -1166,11 +1172,11 @@ let pr_goal_selector ~toplevel s =
     let prtac (t:atomic_tactic_expr) =
       let pr = {
         pr_tactic = (fun _ _ -> str "<tactic>");
-        pr_constr = (fun c -> pr_econstr_env env sigma c);
-        pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
-        pr_lconstr = (fun c -> pr_leconstr_env env sigma c);
-        pr_pattern = pr_constr_pattern_env env sigma;
-        pr_lpattern = pr_lconstr_pattern_env env sigma;
+        pr_constr = pr_econstr_env;
+        pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
+        pr_lconstr = pr_leconstr_env;
+        pr_pattern = pr_constr_pattern_env;
+        pr_lpattern = pr_lconstr_pattern_env;
         pr_constant = pr_evaluable_reference_env env;
         pr_reference = pr_located pr_ltac_constant;
         pr_name = pr_id;
@@ -1180,7 +1186,7 @@ let pr_goal_selector ~toplevel s =
         pr_alias = (fun _ _ _ -> assert false);
       }
       in
-      pr_atom pr strip_prod_binders_constr tag_atomic_tactic_expr t
+      pr_atom env sigma pr strip_prod_binders_constr tag_atomic_tactic_expr t
     in
     prtac t
 
@@ -1188,9 +1194,9 @@ let pr_goal_selector ~toplevel s =
 
   let pr_glb_generic = Pputils.pr_glb_generic
 
-  let pr_raw_extend _ = pr_raw_extend_rec pr_raw_tactic_level
+  let pr_raw_extend env sigma = pr_raw_extend_rec @@ pr_raw_tactic_level env sigma
 
-  let pr_glob_extend env = pr_glob_extend_rec (pr_glob_tactic_level env)
+  let pr_glob_extend env sigma = pr_glob_extend_rec (pr_glob_tactic_level env)
 
   let pr_alias pr lev key args =
     pr_alias_gen (fun _ arg -> pr arg) lev key args
@@ -1209,16 +1215,17 @@ let declare_extra_genarg_pprule wit
     | _          -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.")
   end;
   let f x =
-    Genprint.PrinterBasic (fun () ->
-        f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in
+    Genprint.PrinterBasic (fun env sigma ->
+        f env sigma pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in
   let g x =
-    Genprint.PrinterBasic (fun () ->
-    let env = Global.env () in
-    g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x)
+    Genprint.PrinterBasic (fun env sigma ->
+    g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env))
+      (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env))
+      (fun env sigma -> pr_glob_tactic_level env) x)
   in
   let h x =
     Genprint.TopPrinterNeedsContext (fun env sigma ->
-        h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") x)
+        h env sigma pr_econstr_env pr_leconstr_env (fun _env _sigma _ _ -> str "<tactic>") x)
   in
   Genprint.register_print0 wit f g h
 
@@ -1235,27 +1242,28 @@ let declare_extra_genarg_pprule_with_level wit
     PrinterNeedsLevel {
         default_already_surrounded = default_surrounded;
         default_ensure_surrounded = default_non_surrounded;
-        printer = (fun n ->
-          f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level n x) } in
+        printer = (fun env sigma n ->
+          f env sigma pr_constr_expr pr_lconstr_expr pr_raw_tactic_level n x) } in
   let g x =
-    let env = Global.env () in
     PrinterNeedsLevel {
         default_already_surrounded = default_surrounded;
         default_ensure_surrounded = default_non_surrounded;
-        printer = (fun n ->
-          g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) n x) }
+        printer = (fun env sigma n ->
+          g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env))
+            (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env))
+            (fun env sigma -> pr_glob_tactic_level env) n x) }
   in
   let h x =
     TopPrinterNeedsContextAndLevel {
         default_already_surrounded = default_surrounded;
         default_ensure_surrounded = default_non_surrounded;
         printer = (fun env sigma n ->
-          h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") n x) }
+          h env sigma pr_econstr_env pr_leconstr_env (fun _env _sigma _ _ -> str "<tactic>") n x) }
   in
   Genprint.register_print0 wit f g h
 
 let declare_extra_vernac_genarg_pprule wit f =
-  let f x = Genprint.PrinterBasic (fun () -> f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in
+  let f x = Genprint.PrinterBasic (fun env sigma -> f env sigma pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in
   Genprint.register_vernac_print0 wit f
 
 (** Registering *)
@@ -1265,8 +1273,8 @@ let pr_intro_pattern_env p = Genprint.TopPrinterNeedsContext (fun env sigma ->
   Miscprint.pr_intro_pattern print_constr p)
 
 let pr_red_expr_env r = Genprint.TopPrinterNeedsContext (fun env sigma ->
-  pr_red_expr (pr_econstr_env env sigma, pr_leconstr_env env sigma,
-               pr_evaluable_reference_env env, pr_constr_pattern_env env sigma) r)
+  pr_red_expr env sigma (pr_econstr_env, pr_leconstr_env,
+                         pr_evaluable_reference_env env, pr_constr_pattern_env) r)
 
 let pr_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma ->
   let sigma, bl = bl env sigma in
@@ -1292,19 +1300,18 @@ let make_constr_printer f c =
       Genprint.default_ensure_surrounded = Ppconstr.lsimpleconstr;
       Genprint.printer = (fun env sigma n -> f env sigma n c)}
 
-let lift f a = Genprint.PrinterBasic (fun () -> f a)
+let lift f a = Genprint.PrinterBasic (fun env sigma -> f a)
+let lift_env f a = Genprint.PrinterBasic (fun env sigma -> f env sigma a)
 let lift_top f a = Genprint.TopPrinterBasic (fun () -> f a)
 
 let register_basic_print0 wit f g h =
   Genprint.register_print0 wit (lift f) (lift g) (lift_top h)
 
 
-let pr_glob_constr_pptac c =
-  let _, env = Pfedit.get_current_context () in
+let pr_glob_constr_pptac env sigma c =
   pr_glob_constr_env env c
 
-let pr_lglob_constr_pptac c =
-  let _, env = Pfedit.get_current_context () in
+let pr_lglob_constr_pptac env sigma c =
   pr_lglob_constr_env env c
 
 let () =
@@ -1318,8 +1325,8 @@ let () =
   register_basic_print0 wit_var pr_lident pr_lident pr_id;
   register_print0
     wit_intro_pattern
-    (lift (Miscprint.pr_intro_pattern pr_constr_expr))
-    (lift (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr_pptac c)))
+    (lift_env (fun env sigma -> Miscprint.pr_intro_pattern @@ pr_constr_expr env sigma))
+    (lift_env (fun env sigma -> Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr_pptac env sigma c)))
     pr_intro_pattern_env;
   Genprint.register_print0
     wit_clause_dft_concl
@@ -1329,47 +1336,55 @@ let () =
   ;
   Genprint.register_print0
     wit_constr
-    (lift Ppconstr.pr_lconstr_expr)
-    (lift (fun (c, _) -> pr_lglob_constr_pptac c))
+    (lift_env Ppconstr.pr_lconstr_expr)
+    (lift_env (fun env sigma (c, _) -> pr_lglob_constr_pptac env sigma c))
     (make_constr_printer Printer.pr_econstr_n_env)
   ;
   Genprint.register_print0
     wit_uconstr
-    (lift Ppconstr.pr_constr_expr)
-    (lift (fun (c,_) -> pr_glob_constr_pptac c))
+    (lift_env Ppconstr.pr_constr_expr)
+    (lift_env (fun env sigma (c,_) -> pr_glob_constr_pptac env sigma c))
     (make_constr_printer Printer.pr_closed_glob_n_env)
   ;
   Genprint.register_print0
     wit_open_constr
-    (lift Ppconstr.pr_constr_expr)
-    (lift (fun (c, _) -> pr_glob_constr_pptac c))
+    (lift_env Ppconstr.pr_constr_expr)
+    (lift_env (fun env sigma (c, _) -> pr_glob_constr_pptac env sigma c))
     (make_constr_printer Printer.pr_econstr_n_env)
   ;
   Genprint.register_print0
     wit_red_expr
-    (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_qualid, pr_constr_pattern_expr)))
-    (lift (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac)))
+    (lift_env (fun env sigma -> pr_red_expr env sigma (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_qualid, pr_constr_pattern_expr)))
+    (lift_env (fun env sigma -> pr_red_expr env sigma
+                  ((fun env sigma -> pr_and_constr_expr @@ pr_glob_constr_pptac env sigma),
+                   (fun env sigma -> pr_and_constr_expr @@ pr_lglob_constr_pptac env sigma),
+                   pr_or_var (pr_and_short_name pr_evaluable_reference),
+                   (fun env sigma -> pr_pat_and_constr_expr @@ pr_glob_constr_pptac env sigma))))
     pr_red_expr_env
   ;
   register_basic_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
   register_print0 wit_bindings
-    (lift (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr))
-    (lift (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)))
+    (lift_env (fun env sigma -> Miscprint.pr_bindings_no_with (pr_constr_expr env sigma)
+                  (pr_lconstr_expr env sigma)))
+    (lift_env (fun env sigma -> Miscprint.pr_bindings_no_with (pr_and_constr_expr @@ pr_glob_constr_pptac env sigma) (pr_and_constr_expr @@ pr_lglob_constr_pptac env sigma)))
     pr_bindings_env
   ;
   register_print0 wit_constr_with_bindings
-    (lift (pr_with_bindings pr_constr_expr pr_lconstr_expr))
-    (lift (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)))
+    (lift_env (fun env sigma -> pr_with_bindings (pr_constr_expr env sigma) (pr_lconstr_expr env sigma)))
+    (lift_env (fun env sigma -> pr_with_bindings (pr_and_constr_expr @@ pr_glob_constr_pptac env sigma)
+              (pr_and_constr_expr @@ pr_lglob_constr_pptac env sigma)))
     pr_with_bindings_env
   ;
   register_print0 wit_open_constr_with_bindings
-    (lift (pr_with_bindings pr_constr_expr pr_lconstr_expr))
-    (lift (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)))
+    (lift_env (fun env sigma -> pr_with_bindings (pr_constr_expr env sigma) (pr_lconstr_expr env sigma)))
+    (lift_env (fun env sigma -> pr_with_bindings (pr_and_constr_expr @@ pr_glob_constr_pptac env sigma)
+                  (pr_and_constr_expr @@ pr_lglob_constr_pptac env sigma)))
     pr_with_bindings_env
   ;
   register_print0 Tacarg.wit_destruction_arg
-    (lift (pr_destruction_arg pr_constr_expr pr_lconstr_expr))
-    (lift (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)))
+    (lift_env (fun env sigma -> pr_destruction_arg (pr_constr_expr env sigma) (pr_lconstr_expr env sigma)))
+    (lift_env (fun env sigma -> pr_destruction_arg (pr_and_constr_expr @@ pr_glob_constr_pptac env sigma)
+                  (pr_and_constr_expr @@ pr_lglob_constr_pptac env sigma)))
     pr_destruction_arg_env
   ;
   register_basic_print0 Stdarg.wit_int int int int;
@@ -1379,12 +1394,12 @@ let () =
   register_basic_print0 Stdarg.wit_string qstring qstring qstring
 
 let () =
-  let printer _ _ prtac = prtac in
+  let printer env sigma _ _ prtac = prtac env sigma in
   declare_extra_genarg_pprule_with_level wit_tactic printer printer printer
   ltop (0,E)
 
 let () =
-  let pr_unit _ _ _ _ () = str "()" in
-  let printer _ _ prtac = prtac in
+  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)
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index bc47036d92..70af09833d 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -26,40 +26,46 @@ type 'a grammar_tactic_prod_item_expr =
 | TacNonTerm of ('a * Names.Id.t option) Loc.located
 
 type 'a raw_extra_genarg_printer =
-    (constr_expr -> Pp.t) ->
-    (constr_expr -> Pp.t) ->
-    (tolerability -> raw_tactic_expr -> Pp.t) ->
-    'a -> Pp.t
+  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) ->
+  'a -> Pp.t
 
 type 'a glob_extra_genarg_printer =
-    (glob_constr_and_expr -> Pp.t) ->
-    (glob_constr_and_expr -> Pp.t) ->
-    (tolerability -> glob_tactic_expr -> Pp.t) ->
-    'a -> Pp.t
+  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) ->
+  'a -> Pp.t
 
 type 'a extra_genarg_printer =
-    (EConstr.t -> Pp.t) ->
-    (EConstr.t -> Pp.t) ->
-    (tolerability -> Val.t -> Pp.t) ->
-    'a -> Pp.t
+  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) ->
+  'a -> Pp.t
 
 type 'a raw_extra_genarg_printer_with_level =
-    (constr_expr -> Pp.t) ->
-    (constr_expr -> Pp.t) ->
-    (tolerability -> raw_tactic_expr -> Pp.t) ->
-    tolerability -> 'a -> Pp.t
+  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
 
 type 'a glob_extra_genarg_printer_with_level =
-    (glob_constr_and_expr -> Pp.t) ->
-    (glob_constr_and_expr -> Pp.t) ->
-    (tolerability -> glob_tactic_expr -> Pp.t) ->
-    tolerability -> 'a -> Pp.t
+  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
 
 type 'a extra_genarg_printer_with_level =
-    (EConstr.constr -> Pp.t) ->
-    (EConstr.constr -> Pp.t) ->
-    (tolerability -> Val.t -> Pp.t) ->
-    tolerability -> 'a -> Pp.t
+  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
 
 val declare_extra_genarg_pprule :
   ('a, 'b, 'c) genarg_type ->
@@ -91,12 +97,13 @@ val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
 
 val pr_with_occurrences :
   ('a -> Pp.t) -> 'a Locus.with_occurrences -> Pp.t
-val pr_red_expr :
-  ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) ->
+val pr_red_expr : env -> Evd.evar_map ->
+  (env -> Evd.evar_map -> 'a -> Pp.t) * (env -> Evd.evar_map -> 'a -> Pp.t) * ('b -> Pp.t) * (env -> Evd.evar_map -> 'c -> Pp.t) ->
   ('a,'b,'c) Genredexpr.red_expr_gen -> Pp.t
 val pr_may_eval :
-  ('a -> Pp.t) -> ('a -> Pp.t) -> ('b -> Pp.t) ->
-  ('c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t
+  env -> Evd.evar_map ->
+  (env -> Evd.evar_map -> 'a -> Pp.t) -> (env -> Evd.evar_map -> 'a -> Pp.t) -> ('b -> Pp.t) ->
+  (env -> Evd.evar_map -> 'c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t
 
 val pr_and_short_name : ('a -> Pp.t) -> 'a Genredexpr.and_short_name -> Pp.t
 
@@ -111,14 +118,14 @@ val pr_clauses : (* default: *) bool option ->
   ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t
   (* Some true = default is concl; Some false = default is all; None = no default *)
 
-val pr_raw_generic : env -> rlevel generic_argument -> Pp.t
+val pr_raw_generic : env -> Evd.evar_map -> rlevel generic_argument -> Pp.t
 
-val pr_glb_generic : env -> glevel generic_argument -> Pp.t
+val pr_glb_generic : env -> Evd.evar_map -> glevel generic_argument -> Pp.t
 
-val pr_raw_extend: env -> int ->
+val pr_raw_extend: env -> Evd.evar_map -> int ->
   ml_tactic_entry -> raw_tactic_arg list -> Pp.t
 
-val pr_glob_extend: env -> int ->
+val pr_glob_extend: env -> Evd.evar_map -> int ->
   ml_tactic_entry -> glob_tactic_arg list -> Pp.t
 
 val pr_extend :
@@ -131,9 +138,9 @@ val pr_alias : (Val.t -> Pp.t) ->
 
 val pr_ltac_constant : ltac_constant -> Pp.t
 
-val pr_raw_tactic : raw_tactic_expr -> Pp.t
+val pr_raw_tactic : env -> Evd.evar_map -> raw_tactic_expr -> Pp.t
 
-val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> Pp.t
+val pr_raw_tactic_level : env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t
 
 val pr_glob_tactic : env -> glob_tactic_expr -> Pp.t
 
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 99b9e881f6..52a83a038f 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -19,11 +19,9 @@ let prtac x =
   Pptactic.pr_glob_tactic (Global.env()) x
 let prmatchpatt env sigma hyp =
   Pptactic.pr_match_pattern (Printer.pr_constr_pattern_env env sigma) hyp
-let prmatchrl rl =
+let prmatchrl env sigma rl =
   Pptactic.pr_match_rule false (Pptactic.pr_glob_tactic (Global.env()))
-    (fun (_,p) ->
-       let sigma, env = Pfedit.get_current_context () in
-       Printer.pr_constr_pattern_env env sigma p) rl
+    (fun (_,p) -> Printer.pr_constr_pattern_env env sigma p) rl
 
 (* This module intends to be a beginning of debugger for tactic expressions.
    Currently, it is quite simple and we can hope to have, in the future, a more
@@ -246,13 +244,13 @@ let db_constr debug env sigma c =
   else return ()
 
 (* Prints the pattern rule *)
-let db_pattern_rule debug num r =
+let db_pattern_rule debug env sigma num r =
   let open Proofview.NonLogical in
   is_debug debug >>= fun db ->
   if db then
   begin
     msg_tac_debug (str "Pattern rule " ++ int num ++ str ":" ++ fnl () ++
-      str "|" ++ spc () ++ prmatchrl r)
+      str "|" ++ spc () ++ prmatchrl env sigma r)
   end
   else return ()
 
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index 91e8510b92..74ea4e6b74 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -40,7 +40,7 @@ val db_constr : debug_info -> env -> evar_map -> constr -> unit Proofview.NonLog
 
 (** Prints the pattern rule *)
 val db_pattern_rule :
-  debug_info -> int -> (Genintern.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t
+  debug_info -> env -> evar_map -> int -> (Genintern.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t
 
 (** Prints a matched hypothesis *)
 val db_matched_hyp :