Stop accessing proof env via Pfedit in printers

This should make https://github.com/coq/coq/pull/9129 easier.

41 files changed, 633 insertions, 599 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 4d817625f5..1bdedcaf26 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -196,7 +196,7 @@ module Btauto = struct
         let assign = List.combine penv var in
         let map_msg (key, v) =
           let b = if v then str "true" else str "false" in
-          let sigma, env = Pfedit.get_current_context () in
+          let sigma, env = Tacmach.project gl, Tacmach.pf_env gl in
           let term = Printer.pr_constr_env env sigma key in
           term ++ spc () ++ str ":=" ++ spc () ++ b
         in
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 23cdae7883..048ec56dee 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -27,10 +27,6 @@ let init_size=5
 
 let cc_verbose=ref false
 
-let print_constr t =
-  let sigma, env = Pfedit.get_current_context () in
-  Printer.pr_econstr_env env sigma t
-
 let debug x =
   if !cc_verbose then Feedback.msg_debug (x ())
 
@@ -484,11 +480,11 @@ let rec inst_pattern subst = function
 	(fun spat f -> Appli (f,inst_pattern subst spat))
 	   args t
 
-let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++
-  print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]"
+let pr_idx_term env sigma uf i = str "[" ++ int i ++ str ":=" ++
+  Printer.pr_econstr_env env sigma (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]"
 
-let pr_term t = str "[" ++
-  print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]"
+let pr_term env sigma t = str "[" ++
+  Printer.pr_econstr_env env sigma (EConstr.of_constr (constr_of_term t)) ++ str "]"
 
 let rec add_term state t=
   let uf=state.uf in
@@ -603,16 +599,16 @@ let add_inst state (inst,int_subst) =
 	      begin
 		debug (fun () ->
 		   (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
-                  (str "  [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++
-			   pr_term s ++ str " == " ++ pr_term t ++ str "]"));
+                  (str "  [" ++ Printer.pr_econstr_env state.env state.sigma (EConstr.of_constr prf) ++ str " : " ++
+                           pr_term state.env state.sigma s ++ str " == " ++ pr_term state.env state.sigma t ++ str "]"));
 		add_equality state prf s t
 	      end
 	    else
 	      begin
 		debug (fun () ->
 		   (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
-                  (str "  [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++
-			   pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
+                  (str "  [" ++ Printer.pr_econstr_env state.env state.sigma (EConstr.of_constr prf) ++ str " : " ++
+                           pr_term state.env state.sigma s ++ str " <> " ++ pr_term state.env state.sigma t ++ str "]"));
 		add_disequality state (Hyp prf) s t
 	      end
   end
@@ -640,8 +636,8 @@ let join_path uf i j=
   min_path (down_path uf i [],down_path uf j [])
 
 let union state i1 i2 eq=
-  debug (fun () -> str "Linking " ++ pr_idx_term state.uf i1 ++
-		 str " and " ++ pr_idx_term state.uf i2 ++ str ".");
+  debug (fun () -> str "Linking " ++ pr_idx_term state.env state.sigma state.uf i1 ++
+                 str " and " ++ pr_idx_term state.env state.sigma state.uf i2 ++ str ".");
   let r1= get_representative state.uf i1
   and r2= get_representative state.uf i2 in
     link state.uf i1 i2 eq;
@@ -681,8 +677,8 @@ let union state i1 i2 eq=
 
 let merge eq state = (* merge and no-merge *)
   debug
-    (fun () -> str "Merging " ++ pr_idx_term state.uf eq.lhs ++
-       str " and " ++ pr_idx_term state.uf eq.rhs ++ str ".");
+    (fun () -> str "Merging " ++ pr_idx_term state.env state.sigma state.uf eq.lhs ++
+       str " and " ++ pr_idx_term state.env state.sigma state.uf eq.rhs ++ str ".");
   let uf=state.uf in
   let i=find uf eq.lhs
   and j=find uf eq.rhs in
@@ -694,7 +690,7 @@ let merge eq state = (* merge and no-merge *)
 
 let update t state = (* update 1 and 2 *)
   debug
-    (fun () -> str "Updating term " ++ pr_idx_term state.uf t ++ str ".");
+    (fun () -> str "Updating term " ++ pr_idx_term state.env state.sigma state.uf t ++ str ".");
   let (i,j) as sign = signature state.uf t in
   let (u,v) = subterms state.uf t in
   let rep = get_representative state.uf i in
@@ -756,7 +752,7 @@ let process_constructor_mark t i rep pac state =
 
 let process_mark t m state =
   debug
-    (fun () -> str "Processing mark for term " ++ pr_idx_term state.uf t ++ str ".");
+    (fun () -> str "Processing mark for term " ++ pr_idx_term state.env state.sigma state.uf t ++ str ".");
   let i=find state.uf t in
   let rep=get_representative state.uf i in
     match m with
@@ -777,8 +773,8 @@ let check_disequalities state =
           else (str "No", check_aux q)
         in
         let _ = debug
-        (fun () -> str "Checking if " ++ pr_idx_term state.uf dis.lhs ++ str " = " ++
-         pr_idx_term state.uf dis.rhs ++ str " ... " ++ info) in
+        (fun () -> str "Checking if " ++ pr_idx_term state.env state.sigma state.uf dis.lhs ++ str " = " ++
+         pr_idx_term state.env state.sigma state.uf dis.rhs ++ str " ... " ++ info) in
         ans
     | [] -> None
   in
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index d52e83dc31..978969bf59 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -169,7 +169,7 @@ val find_instances : state -> (quant_eq * int array) list
 
 val execute : bool -> state -> explanation option
 
-val pr_idx_term : forest -> int -> Pp.t
+val pr_idx_term : Environ.env -> Evd.evar_map -> forest -> int -> Pp.t
 
 val empty_forest: unit -> forest
 
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 1f1fa9c99a..4f46f8327a 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -94,65 +94,65 @@ let pinject p c n a =
    p_rhs=nth_arg p.p_rhs (n-a);
    p_rule=Inject(p,c,n,a)}
 
-let rec equal_proof uf i j=
-  debug (fun () -> str "equal_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+let rec equal_proof env sigma uf i j=
+  debug (fun () -> str "equal_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
   if i=j then prefl (term uf i) else
     let (li,lj)=join_path uf i j in
-    ptrans (path_proof uf i li) (psym (path_proof uf j lj))
+    ptrans (path_proof env sigma uf i li) (psym (path_proof env sigma uf j lj))
       
-and edge_proof uf ((i,j),eq)=
-  debug (fun () -> str "edge_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
-  let pi=equal_proof uf i eq.lhs in
-  let pj=psym (equal_proof uf j eq.rhs) in
+and edge_proof env sigma uf ((i,j),eq)=
+  debug (fun () -> str "edge_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
+  let pi=equal_proof env sigma uf i eq.lhs in
+  let pj=psym (equal_proof env sigma uf j eq.rhs) in
   let pij=
     match eq.rule with
       Axiom (s,reversed)->
 	if reversed then psymax (axioms uf) s
 	else pax (axioms uf) s
-    | Congruence ->congr_proof uf eq.lhs eq.rhs
+    | Congruence ->congr_proof env sigma uf eq.lhs eq.rhs
     | Injection (ti,ipac,tj,jpac,k) -> (* pi_k ipac = p_k jpac *) 
-      let p=ind_proof uf ti ipac tj jpac in
+      let p=ind_proof env sigma uf ti ipac tj jpac in
       let cinfo= get_constructor_info uf ipac.cnode in
       pinject p cinfo.ci_constr cinfo.ci_nhyps k in  
   ptrans (ptrans pi pij) pj
   
-and constr_proof uf i ipac=
-  debug (fun () -> str "constr_proof " ++ pr_idx_term uf i ++ brk (1,20));
+and constr_proof env sigma uf i ipac=
+  debug (fun () -> str "constr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20));
   let t=find_oldest_pac uf i ipac in
-  let eq_it=equal_proof uf i t in
+  let eq_it=equal_proof env sigma uf i t in
   if ipac.args=[] then
     eq_it
   else
     let fipac=tail_pac ipac in
     let (fi,arg)=subterms uf t in
     let targ=term uf arg in
-    let p=constr_proof uf fi fipac in
+    let p=constr_proof env sigma uf fi fipac in
     ptrans eq_it (pcongr p (prefl targ))
       
-and path_proof uf i l=
-  debug (fun () -> str "path_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ str "{" ++
+and path_proof env sigma uf i l=
+  debug (fun () -> str "path_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ str "{" ++
 	   (prlist_with_sep (fun () -> str ",") (fun ((_,j),_) -> int j) l) ++ str "}");
   match l with
   | [] -> prefl (term uf i)
-  | x::q->ptrans (path_proof uf (snd (fst x)) q) (edge_proof uf x)
+  | x::q->ptrans (path_proof env sigma uf (snd (fst x)) q) (edge_proof env sigma uf x)
     
-and congr_proof uf i j=
-  debug (fun () -> str "congr_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+and congr_proof env sigma uf i j=
+  debug (fun () -> str "congr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
   let (i1,i2) = subterms uf i
   and (j1,j2) = subterms uf j in
-  pcongr (equal_proof uf i1 j1) (equal_proof uf i2 j2)
+  pcongr (equal_proof env sigma uf i1 j1) (equal_proof env sigma uf i2 j2)
     
-and ind_proof uf i ipac j jpac=
-   debug (fun () -> str "ind_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
-  let p=equal_proof uf i j
-  and p1=constr_proof uf i ipac
-  and p2=constr_proof uf j jpac in
+and ind_proof env sigma uf i ipac j jpac=
+   debug (fun () -> str "ind_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
+  let p=equal_proof env sigma uf i j
+  and p1=constr_proof env sigma uf i ipac
+  and p2=constr_proof env sigma uf j jpac in
   ptrans (psym p1) (ptrans p p2)
 
-let build_proof uf=
+let build_proof env sigma uf=
   function
-  | `Prove (i,j) -> equal_proof uf i j
-  | `Discr (i,ci,j,cj)-> ind_proof uf i ci j cj
+  | `Prove (i,j) -> equal_proof env sigma uf i j
+  | `Discr (i,ci,j,cj)-> ind_proof env sigma uf i ci j cj
 
 
 
diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
index bebef241e1..9ea31259c1 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
@@ -41,20 +41,20 @@ val pinject :  proof -> pconstructor -> int -> int -> proof
 
 (** Proof building functions *)
 
-val equal_proof : forest -> int -> int -> proof
+val equal_proof : Environ.env -> Evd.evar_map -> forest -> int -> int -> proof
 
-val edge_proof : forest -> (int*int)*equality -> proof
+val edge_proof : Environ.env -> Evd.evar_map -> forest -> (int*int)*equality -> proof
 
-val path_proof : forest -> int -> ((int*int)*equality) list -> proof
+val path_proof : Environ.env -> Evd.evar_map -> forest -> int -> ((int*int)*equality) list -> proof
 
-val congr_proof :  forest -> int -> int -> proof
+val congr_proof : Environ.env -> Evd.evar_map -> forest -> int -> int -> proof
 
-val ind_proof : forest -> int -> pa_constructor -> int -> pa_constructor -> proof
+val ind_proof : Environ.env -> Evd.evar_map -> forest -> int -> pa_constructor -> int -> pa_constructor -> proof
 
 (** Main proof building function *)
 
 val build_proof :
-  forest ->
+  Environ.env -> Evd.evar_map -> forest ->
   [ `Discr of int * pa_constructor * int * pa_constructor
   | `Prove of int * int ] -> proof
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 5778acce0a..50fc2448fc 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -433,7 +433,7 @@ let cc_tactic depth additionnal_terms =
 	debug (fun () -> Pp.str "Goal solved, generating proof ...");
 	match reason with
 	  Discrimination (i,ipac,j,jpac) ->
-	    let p=build_proof uf (`Discr (i,ipac,j,jpac)) in
+            let p=build_proof (Tacmach.New.pf_env gl) sigma uf (`Discr (i,ipac,j,jpac)) in
 	    let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
 	    discriminate_tac cstr p
 	| Incomplete ->
@@ -462,7 +462,8 @@ let cc_tactic depth additionnal_terms =
 		 Pp.str "  replacing metavariables by arbitrary terms.");
 	    Tacticals.New.tclFAIL 0 (str "Incomplete")
 	| Contradiction dis ->
-	    let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in
+      let env = Proofview.Goal.env gl in
+            let p=build_proof env sigma uf (`Prove (dis.lhs,dis.rhs)) in
 	    let ta=term uf dis.lhs and tb=term uf dis.rhs in
 	    match dis.rule with
 	      Goal -> proof_tac p
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 5958fe8203..01b18e2f30 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -235,7 +235,7 @@ let print_cmap map=
       str "| " ++
       prlist Printer.pr_global l ++
       str " : " ++
-      Ppconstr.pr_constr_expr xc ++
+      Ppconstr.pr_constr_expr env sigma xc ++
       cut () ++
       s in
     (v 0
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 34283c49c3..16f376931e 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -45,10 +45,6 @@ let observe_tac s tac g = observe_tac_stream (str s) tac g
   *)
 
 
-let pr_leconstr_fp =
-  let sigma, env = Pfedit.get_current_context () in
-  Printer.pr_leconstr_env env sigma
-
 let debug_queue = Stack.create ()
 
 let rec print_debug_queue e = 
@@ -164,7 +160,7 @@ let rec incompatible_constructor_terms sigma t1 t2 =
 	List.exists2 (incompatible_constructor_terms sigma) arg1 arg2
     )
 
-let is_incompatible_eq sigma t =
+let is_incompatible_eq env sigma t =
   let res =
     try
       match EConstr.kind sigma t with
@@ -176,7 +172,7 @@ let is_incompatible_eq sigma t =
 	| _ -> false
     with e when CErrors.noncritical e -> false
   in
-  if res then   observe (str "is_incompatible_eq " ++ pr_leconstr_fp t);
+  if res then   observe (str "is_incompatible_eq " ++ pr_leconstr_env env sigma t);
   res
 
 let change_hyp_with_using msg hyp_id t tac : tactic =
@@ -480,7 +476,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 (* 		    ); *)
 	    raise TOREMOVE;  (* False -> .. useless *)
 	  end
-	else if is_incompatible_eq sigma t_x then raise TOREMOVE (* t_x := C1 ... =  C2 ... *)
+        else if is_incompatible_eq env sigma t_x then raise TOREMOVE (* t_x := C1 ... =  C2 ... *)
 	else if eq_constr sigma t_x coq_True  (* Trivial => we remove this precons *)
 	then
 (* 	    observe (str "In "++Ppconstr.pr_id hyp_id++  *)
@@ -726,7 +722,7 @@ let build_proof
 					  (treat_new_case
 					     ptes_infos
                                              nb_instantiate_partial
-					     (build_proof do_finalize)
+                                             (build_proof env sigma do_finalize)
 					     t
 					     dyn_infos)
 					  g'
@@ -737,7 +733,7 @@ let build_proof
 		    ]
 		    g
 	      in
-	      build_proof do_finalize_t {dyn_infos with info = t} g
+              build_proof env sigma do_finalize_t {dyn_infos with info = t} g
           | Lambda(n,t,b) ->
 	      begin
 		match EConstr.kind sigma (pf_concl g) with
@@ -753,7 +749,7 @@ let build_proof
 			   in
 			   let new_infos = {dyn_infos with info = new_term} in
 			   let do_prove new_hyps =
-			     build_proof do_finalize
+                             build_proof env sigma do_finalize
 			       {new_infos with
 			       	  rec_hyps = new_hyps;
 				  nb_rec_hyps  = List.length new_hyps
@@ -766,7 +762,7 @@ let build_proof
 		      do_finalize dyn_infos g
 	      end
 	  | Cast(t,_,_) ->
-	      build_proof do_finalize {dyn_infos with info = t} g
+              build_proof env sigma do_finalize {dyn_infos with info = t} g
           | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ ->
 	      do_finalize dyn_infos g
 	  | App(_,_) ->
@@ -782,7 +778,7 @@ let build_proof
 			    info = (f,args)
 			}
 		      in
-		      build_proof_args do_finalize new_infos  g
+                      build_proof_args env sigma do_finalize new_infos  g
 		  | Const (c,_) when not (List.mem_f Constant.equal c fnames) ->
 		      let new_infos =
 			{ dyn_infos with
@@ -790,13 +786,13 @@ let build_proof
 			}
 		      in
 (* 		      Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *)
-		      build_proof_args do_finalize new_infos g
+                      build_proof_args env sigma do_finalize new_infos g
 		  | Const _ ->
 		      do_finalize dyn_infos  g
 		  | Lambda _ ->
 		      let new_term =
                         Reductionops.nf_beta env sigma dyn_infos.info in
-		      build_proof do_finalize {dyn_infos with info = new_term}
+                      build_proof env sigma do_finalize {dyn_infos with info = new_term}
 			g
 		  | LetIn _ ->
 		      let new_infos =
@@ -809,11 +805,11 @@ let build_proof
 			     h_reduce_with_zeta (Locusops.onHyp hyp_id))
 			   dyn_infos.rec_hyps;
 			 h_reduce_with_zeta Locusops.onConcl;
-			 build_proof do_finalize new_infos
+                         build_proof env sigma do_finalize new_infos
 			]
 			g
 		  | Cast(b,_,_) ->
-		      build_proof do_finalize {dyn_infos with info = b } g
+                      build_proof env sigma do_finalize {dyn_infos with info = b } g
 		  | Case _ | Fix _ | CoFix _ ->
 		      let new_finalize dyn_infos =
 			let new_infos =
@@ -821,9 +817,9 @@ let build_proof
 			      info = dyn_infos.info,args
 			  }
 			in
-			build_proof_args do_finalize new_infos
+                        build_proof_args env sigma do_finalize new_infos
 		      in
-		      build_proof new_finalize {dyn_infos  with info = f } g
+                      build_proof env sigma new_finalize {dyn_infos  with info = f } g
 	      end
 	  | Fix _ | CoFix _ ->
 	      user_err Pp.(str ( "Anonymous local (co)fixpoints are not handled yet"))
@@ -843,13 +839,13 @@ let build_proof
 		   (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id))
 		   dyn_infos.rec_hyps;
 		 h_reduce_with_zeta Locusops.onConcl;
-		 build_proof do_finalize new_infos
+                 build_proof env sigma do_finalize new_infos
 		] g
 	  | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
-  and build_proof do_finalize dyn_infos g =
+  and build_proof env sigma do_finalize dyn_infos g =
 (*     observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
-    observe_tac_stream (str "build_proof with " ++ pr_leconstr_fp dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
-  and build_proof_args do_finalize dyn_infos (* f_args'  args *) :tactic =
+    observe_tac_stream (str "build_proof with " ++ pr_leconstr_env env sigma dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
+  and build_proof_args env sigma do_finalize dyn_infos (* f_args'  args *) :tactic =
     fun g ->
       let (f_args',args) = dyn_infos.info in
       let tac : tactic =
@@ -865,12 +861,12 @@ let build_proof
 	      let do_finalize dyn_infos =
 		let new_arg = dyn_infos.info in
 		(* 		tclTRYD *)
-		(build_proof_args
+                (build_proof_args env sigma
 		   do_finalize
 		   {dyn_infos with info = (mkApp(f_args',[|new_arg|])), args}
 		)
 	      in
-	      build_proof do_finalize
+              build_proof env sigma do_finalize
 		{dyn_infos with info = arg }
 		g
       in
@@ -882,7 +878,10 @@ let build_proof
 		      finish_proof dyn_infos)
   in
     (* observe_tac "build_proof" *)
-  (build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos)
+  fun g ->
+    let env = pf_env g in
+    let sigma = project g in
+    build_proof env sigma (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos g
 
 
 
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index c4f8843e51..6f67ab4d8b 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -29,10 +29,10 @@ DECLARE PLUGIN "recdef_plugin"
 
 {
 
-let pr_fun_ind_using  prc prlc _ opt_c =
+let pr_fun_ind_using env sigma prc prlc _ opt_c =
   match opt_c with
     | None -> mt ()
-    | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b)
+    | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings (prc env sigma) (prlc env sigma) b)
 
 (* Duplication of printing functions because "'a with_bindings" is
    (internally) not uniform in 'a: indeed constr_with_bindings at the
@@ -47,15 +47,15 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
       let env = Global.env () in
       let evd = Evd.from_env env in
       let (_, b) = b env evd in
-      spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b)
+      spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings (prc env evd) (prlc env evd) b)
 
 }
 
 ARGUMENT EXTEND fun_ind_using
   TYPED AS constr_with_bindings option
   PRINTED BY { pr_fun_ind_using_typed }
-  RAW_PRINTED BY { pr_fun_ind_using }
-  GLOB_PRINTED BY { pr_fun_ind_using }
+  RAW_PRINTED BY { pr_fun_ind_using env sigma }
+  GLOB_PRINTED BY { pr_fun_ind_using env sigma }
 | [ "using" constr_with_bindings(c) ] -> { Some c }
 | [ ] -> { None }
 END
@@ -119,26 +119,26 @@ END
 
 {
 
-let pr_constr_comma_sequence prc _ _ = prlist_with_sep pr_comma prc
+let pr_constr_comma_sequence env sigma prc _ _ = prlist_with_sep pr_comma (prc env sigma)
 
 }
 
 ARGUMENT EXTEND constr_comma_sequence'
   TYPED AS constr list
-  PRINTED BY { pr_constr_comma_sequence }
+  PRINTED BY { pr_constr_comma_sequence env sigma }
 | [ constr(c) "," constr_comma_sequence'(l) ] -> { c::l }
 | [ constr(c) ] -> { [c] }
 END
 
 {
 
-let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc
+let pr_auto_using env sigma prc _prlc _prt = Pptactic.pr_auto_using (prc env sigma)
 
 }
 
 ARGUMENT EXTEND auto_using'
   TYPED AS constr list
-  PRINTED BY { pr_auto_using }
+  PRINTED BY { pr_auto_using env sigma }
 | [ "using" constr_comma_sequence'(l) ] -> { l }
 | [ ] -> { [] }
 END
@@ -170,7 +170,7 @@ END
 {
 
 let () =
-  let raw_printer _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in
+  let raw_printer env sigma _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in
   Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer
 
 }
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 8611dcaf83..f4807954a7 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -353,7 +353,7 @@ let raw_push_named (na,raw_value,raw_typ) env =
            EConstr.push_named (NamedDecl.LocalDef (na, value, typ)) env)
 
 
-let add_pat_variables pat typ env : Environ.env =
+let add_pat_variables sigma pat typ env : Environ.env =
   let rec add_pat_variables env pat typ  : Environ.env =
     observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));
 
@@ -375,7 +375,6 @@ let add_pat_variables pat typ env : Environ.env =
       Context.Rel.fold_outside
 	(fun decl (env,ctxt) ->
            let open Context.Rel.Declaration in
-           let sigma, _ = Pfedit.get_current_context () in
            match decl with
            | LocalAssum ({binder_name=Anonymous},_) | LocalDef ({binder_name=Anonymous},_,_) -> assert false
            | LocalAssum ({binder_name=Name id} as na, t) ->
@@ -476,7 +475,7 @@ let rec pattern_to_term_and_type env typ  = DAst.with_val (function
 *)
 
 
-let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
+let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_return =
   observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt);
   let open CAst in
   match DAst.get rt with
@@ -488,7 +487,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	let args_res : (glob_constr list) build_entry_return =
 	  List.fold_right (* create the arguments lists of constructors and combine them *)
 	    (fun arg ctxt_argsl ->
-	       let arg_res = build_entry_lc env funnames ctxt_argsl.to_avoid arg in
+               let arg_res = build_entry_lc env sigma funnames ctxt_argsl.to_avoid arg in
 	       combine_results combine_args arg_res ctxt_argsl
 	    )
 	    args
@@ -507,7 +506,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 			  | _ -> 
 			      GApp(t,l)
 		in
-		build_entry_lc env funnames avoid (aux f args)
+                build_entry_lc env sigma funnames avoid (aux f args)
 	    | GVar id when Id.Set.mem id funnames ->
 		(* if we have [f t1 ... tn] with [f]$\in$[fnames]
 		   then we create a fresh variable [res],
@@ -571,7 +570,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 		in
 		build_entry_lc
 		  env
-		  funnames
+      sigma
+      funnames
 		  avoid
 		  (mkGLetIn(new_n,v,t,mkGApp(new_b,args)))
 	    | GCases _  | GIf _ | GLetTuple _ ->
@@ -579,7 +579,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 		   we first compute the result from the case and
 		   then combine each of them with each of args one
 		*)
-		let f_res = build_entry_lc env funnames args_res.to_avoid f in
+                let f_res = build_entry_lc env sigma funnames args_res.to_avoid f in
 		combine_results combine_app f_res  args_res
 	    | GCast(b,_) ->
 		(* for an applied cast we just trash the cast part
@@ -587,7 +587,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 
 		   WARNING: We need to restart since [b] itself should be an application term
 		*)
-		build_entry_lc env funnames avoid (mkGApp(b,args))
+                build_entry_lc env sigma funnames avoid (mkGApp(b,args))
 	    | GRec _ -> user_err Pp.(str "Not handled GRec")
 	    | GProd _ -> user_err Pp.(str "Cannot apply a type")
             | GInt _ -> user_err Pp.(str "Cannot apply an integer")
@@ -599,14 +599,14 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	   then the one corresponding to the type
 	   and combine the two result
 	*)
-	let t_res = build_entry_lc env funnames avoid t  in
+        let t_res = build_entry_lc env sigma funnames avoid t  in
 	let new_n =
 	  match n with
 	    | Name _ -> n
 	    | Anonymous -> Name (Indfun_common.fresh_id [] "_x")
 	in
 	let new_env = raw_push_named (new_n,None,t) env in
-	let b_res = build_entry_lc new_env funnames avoid b in
+        let b_res = build_entry_lc new_env sigma funnames avoid b in
 	combine_results (combine_lam new_n) t_res b_res
     | GProd(n,_,t,b) ->
 	(* we first compute the list of constructor
@@ -614,9 +614,9 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	   then the one corresponding to the type
 	   and combine the two result
 	*)
-	let t_res = build_entry_lc env funnames avoid t in
+        let t_res = build_entry_lc env sigma funnames avoid t in
 	let new_env = raw_push_named (n,None,t) env in
-	let b_res = build_entry_lc new_env funnames avoid b in
+        let b_res = build_entry_lc new_env sigma funnames avoid b in
         if List.length t_res.result = 1 && List.length b_res.result = 1
         then combine_results (combine_prod2 n) t_res b_res
         else combine_results (combine_prod n) t_res b_res
@@ -627,7 +627,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	   and combine the two result
 	*)
         let v = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
-	let v_res = build_entry_lc env funnames avoid v in
+        let v_res = build_entry_lc env sigma funnames avoid v in
 	let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
         let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in
         let v_r = Sorts.Relevant in (* TODO relevance *)
@@ -636,14 +636,14 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	      Anonymous -> env
             | Name id -> EConstr.push_named (NamedDecl.LocalDef (make_annot id v_r,v_as_constr,v_type)) env
         in
-	let b_res = build_entry_lc new_env funnames avoid b in
+        let b_res = build_entry_lc new_env sigma funnames avoid b in
 	combine_results (combine_letin n) v_res b_res
     | GCases(_,_,el,brl) ->
 	(* we create the discrimination function
 	   and treat the case itself
 	*)
 	let make_discr = make_discr_match brl in
-	build_entry_lc_from_case env funnames make_discr el brl avoid
+        build_entry_lc_from_case env sigma funnames make_discr el brl avoid
     | GIf(b,(na,e_option),lhs,rhs) ->
 	let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
         let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
@@ -666,7 +666,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	  mkGCases(None,[(b,(Anonymous,None))],brl)
 	in
 	(* 		Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *)
-	build_entry_lc env funnames avoid match_expr
+        build_entry_lc env sigma funnames avoid match_expr
     | GLetTuple(nal,_,b,e) ->
 	begin
 	  let nal_as_glob_constr =
@@ -690,13 +690,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	  assert (Int.equal (Array.length case_pats) 1);
           let br = CAst.make ([],[case_pats.(0)],e) in
 	  let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in
-	  build_entry_lc env funnames avoid match_expr
+          build_entry_lc env sigma funnames avoid match_expr
 
 	end
     | GRec _ -> user_err Pp.(str "Not handled GRec")
     | GCast(b,_) ->
-	build_entry_lc env funnames  avoid b
-and build_entry_lc_from_case env funname make_discr
+        build_entry_lc env sigma funnames  avoid b
+and build_entry_lc_from_case env sigma funname make_discr
     (el:tomatch_tuples)
     (brl:Glob_term.cases_clauses) avoid :
     glob_constr build_entry_return =
@@ -714,7 +714,7 @@ and build_entry_lc_from_case env funname make_discr
 	let case_resl =
 	    List.fold_right
 	      (fun (case_arg,_) ctxt_argsl ->
-		let arg_res = build_entry_lc env funname ctxt_argsl.to_avoid case_arg in
+                let arg_res = build_entry_lc env sigma funname ctxt_argsl.to_avoid case_arg in
 		combine_results combine_args arg_res ctxt_argsl
 	      )
 	      el
@@ -731,7 +731,7 @@ and build_entry_lc_from_case env funname make_discr
 	  List.map
 	    (fun ca ->
 	       let res = build_entry_lc_from_case_term
-	       env types
+               env sigma types
 	       funname (make_discr)
 	       []  brl
 	       case_resl.to_avoid
@@ -748,7 +748,7 @@ and build_entry_lc_from_case env funname make_discr
               [] results
 	}
 
-and build_entry_lc_from_case_term env types funname make_discr patterns_to_prevent brl avoid
+and build_entry_lc_from_case_term env sigma types funname make_discr patterns_to_prevent brl avoid
     matched_expr =
   match brl with
     | [] -> (* computed_branches  *) {result = [];to_avoid = avoid}
@@ -759,14 +759,14 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	(* building a list of precondition stating that we are not in this branch
 	   (will be used in the following recursive calls)
 	*)
-	let new_env = List.fold_right2 add_pat_variables patl types env in
+        let new_env = List.fold_right2 (add_pat_variables sigma) patl types env in
 	let not_those_patterns : (Id.t list -> glob_constr -> glob_constr) list =
 	  List.map2
 	    (fun pat typ ->
 	       fun avoid pat'_as_term ->
 		 let renamed_pat,_,_ = alpha_pat avoid pat in
 		 let pat_ids = get_pattern_id renamed_pat  in
-		 let env_with_pat_ids = add_pat_variables pat typ new_env in
+                 let env_with_pat_ids = add_pat_variables sigma pat typ new_env in
 		   List.fold_right
 		     (fun id acc ->
 			let typ_of_id =
@@ -798,6 +798,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	let brl'_res =
 	  build_entry_lc_from_case_term
 	    env
+      sigma
 	    types
 	    funname
 	    make_discr
@@ -862,7 +863,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	  )
 	in
 	(* We compute the result of the value returned by the branch*)
-	let return_res = build_entry_lc new_env funname new_avoid return in
+        let return_res = build_entry_lc new_env sigma funname new_avoid return in
 	(* and combine it with the preconds computed for this branch *)
 	let this_branch_res =
 	  List.map
@@ -895,8 +896,7 @@ let same_raw_term rt1 rt2 =
     | GRef(r1,_), GRef (r2,_) -> GlobRef.equal r1 r2
     | GHole _, GHole _ -> true
     | _ -> false
-let decompose_raw_eq lhs rhs = 
-  let _, env = Pfedit.get_current_context () in
+let decompose_raw_eq env lhs rhs =
   let rec decompose_raw_eq lhs rhs acc =
     observe (str "decomposing eq for " ++ pr_glob_constr_env env lhs ++ str " " ++ pr_glob_constr_env env rhs);
     let (rhd,lrhs) = glob_decompose_app rhs in
@@ -1086,7 +1086,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		  ->
 	      begin
 		try 
-		  let l = decompose_raw_eq rt1 rt2 in 
+                  let l = decompose_raw_eq env rt1 rt2 in
 		  if List.length l > 1 
 		  then 
 		    let new_rt =
@@ -1346,7 +1346,7 @@ let do_build_inductive
         resolve_and_replace_implicits ~expected_type:(Pretyping.OfType t) env evd rt
       ) rta
   in
-  let resa = Array.map (build_entry_lc env funnames_as_set []) rta in
+  let resa = Array.map (build_entry_lc env evd funnames_as_set []) rta in
   let env_with_graphs =
     let rel_arity i funargs =  (* Rebuilding arities (with parameters) *)
       let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list  =
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 88546e9ae8..e34323abf4 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -276,12 +276,10 @@ let subst_Function (subst,finfos) =
 
 let discharge_Function (_,finfos) = Some finfos
 
-let pr_ocst c =
-  let sigma, env = Pfedit.get_current_context () in
+let pr_ocst env sigma c =
   Option.fold_right (fun v acc -> Printer.pr_lconstr_env env sigma (mkConst v)) c (mt ())
 
-let pr_info f_info =
-  let sigma, env = Pfedit.get_current_context () in
+let pr_info env sigma f_info =
   str "function_constant := " ++
   Printer.pr_lconstr_env env sigma (mkConst f_info.function_constant)++ fnl () ++
   str "function_constant_type := " ++
@@ -289,17 +287,17 @@ let pr_info f_info =
      Printer.pr_lconstr_env env sigma
        (fst (Typeops.type_of_global_in_context env (ConstRef f_info.function_constant)))
    with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
-  str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
-  str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
-  str "correctness_lemma := " ++ pr_ocst f_info.correctness_lemma ++ fnl () ++
-  str "rect_lemma := " ++ pr_ocst f_info.rect_lemma ++ fnl () ++
-  str "rec_lemma := " ++ pr_ocst f_info.rec_lemma ++ fnl () ++
-  str "prop_lemma := " ++ pr_ocst f_info.prop_lemma ++ fnl () ++
+  str "equation_lemma := " ++ pr_ocst env sigma f_info.equation_lemma ++ fnl () ++
+  str "completeness_lemma :=" ++ pr_ocst env sigma f_info.completeness_lemma ++ fnl () ++
+  str "correctness_lemma := " ++ pr_ocst env sigma f_info.correctness_lemma ++ fnl () ++
+  str "rect_lemma := " ++ pr_ocst env sigma f_info.rect_lemma ++ fnl () ++
+  str "rec_lemma := " ++ pr_ocst env sigma f_info.rec_lemma ++ fnl () ++
+  str "prop_lemma := " ++ pr_ocst env sigma f_info.prop_lemma ++ fnl () ++
   str "graph_ind := " ++ Printer.pr_lconstr_env env sigma (mkInd f_info.graph_ind) ++ fnl ()
 
-let pr_table tb =
+let pr_table env sigma tb =
   let l = Cmap_env.fold (fun k v acc -> v::acc) tb [] in
-  Pp.prlist_with_sep fnl pr_info l
+  Pp.prlist_with_sep fnl (pr_info env sigma) l
 
 let in_Function : function_info -> Libobject.obj =
   let open Libobject in
@@ -358,7 +356,7 @@ let add_Function is_general f =
   in
   update_Function finfos
 
-let pr_table () = pr_table !from_function
+let pr_table env sigma = pr_table env sigma !from_function
 (*********************************)
 (* Debuging *)
 let functional_induction_rewrite_dependent_proofs = ref true
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 4ec3131518..12facc5744 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -83,8 +83,8 @@ val update_Function : function_info -> unit
 
 
 (** debugging *)
-val pr_info : function_info -> Pp.t
-val pr_table : unit -> Pp.t
+val pr_info : Environ.env -> Evd.evar_map -> function_info -> Pp.t
+val pr_table : Environ.env -> Evd.evar_map -> Pp.t
 
 
 (* val function_debug : bool ref  *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 988cae8fbf..e19741a4e9 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -58,10 +58,6 @@ let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global
 let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"]
 let arith_Lt  = ["Coq"; "Arith";"Lt"]
 
-let pr_leconstr_rd =
-  let sigma, env = Pfedit.get_current_context () in
-  Printer.pr_leconstr_env env sigma
-
 let coq_init_constant s =
   EConstr.of_constr (
     UnivGen.constr_of_monomorphic_global @@
@@ -303,7 +299,7 @@ let tclUSER_if_not_mes concl_tac is_mes names_to_suppress =
 (* [check_not_nested forbidden e] checks that [e] does not contains any variable 
    of [forbidden]
 *)
-let check_not_nested sigma forbidden e =
+let check_not_nested env sigma forbidden e =
   let rec check_not_nested e =  
     match EConstr.kind sigma e with 
       | Rel _ -> ()
@@ -330,7 +326,6 @@ let check_not_nested sigma forbidden e =
   try 
     check_not_nested e 
   with UserError(_,p) -> 
-    let _, env = Pfedit.get_current_context () in
     user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr_env env sigma e ++ str " " ++ p)
 
 (* ['a info] contains the local information for traveling *)
@@ -446,7 +441,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
     | Prod _ -> 
       begin
 	try
-	  check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
+          check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
 	  jinfo.otherS () expr_info continuation_tac expr_info g
 	with e when CErrors.noncritical e ->
           user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
@@ -454,7 +449,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
     | Lambda(n,t,b) ->
       begin
 	try
-	  check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
+          check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
 	  jinfo.otherS () expr_info continuation_tac expr_info g
 	with e when CErrors.noncritical e ->
           user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
@@ -507,10 +502,11 @@ and travel_args jinfo is_final continuation_tac infos =
       in
       travel jinfo new_continuation_tac 
 	{infos with info=arg;is_final=false} 
-and travel jinfo continuation_tac expr_info = 
-  observe_tac 
-    (str jinfo.message ++ pr_leconstr_rd expr_info.info)
-    (travel_aux jinfo continuation_tac expr_info)
+and travel jinfo continuation_tac expr_info =
+  fun g ->
+  observe_tac
+    (str jinfo.message ++ Printer.pr_leconstr_env (pf_env g) (project g) expr_info.info)
+    (travel_aux jinfo continuation_tac expr_info) g
 
 (* Termination proof *) 
 
@@ -652,7 +648,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info g =
   let new_forbidden = 
     let forbid = 
       try 
-	check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) b;
+        check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids) b;
 	true
       with e when CErrors.noncritical e -> false
     in
@@ -711,7 +707,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
   let sigma = project g in
   let f_is_present =
     try
-      check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) a;
+      check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids) a;
       false
     with e when CErrors.noncritical e ->
       true
@@ -740,7 +736,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
     
 let terminate_app_rec (f,args) expr_info continuation_tac _ g =
   let sigma = project g in
-  List.iter (check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids))
+  List.iter (check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids))
     args;
   begin
     try 
@@ -987,13 +983,19 @@ let rec intros_values_eq expr_info acc =
     ))
 
 let equation_others _ expr_info continuation_tac infos = 
+  fun g ->
+  let env = pf_env g in
+  let sigma = project g in
   if expr_info.is_final && expr_info.is_main_branch 
-  then 
-    observe_tac (str "equation_others (cont_tac +intros) " ++ pr_leconstr_rd expr_info.info)
+  then
+    observe_tac (str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr_env env sigma expr_info.info)
 		(tclTHEN 
       (continuation_tac infos) 
-      (observe_tac (str "intros_values_eq equation_others "  ++ pr_leconstr_rd expr_info.info) (intros_values_eq expr_info [])))
-  else observe_tac (str "equation_others (cont_tac) " ++ pr_leconstr_rd expr_info.info) (continuation_tac infos)
+      (fun g ->
+       let env = pf_env g in
+       let sigma = project g in
+       observe_tac (str "intros_values_eq equation_others "  ++ Printer.pr_leconstr_env env sigma expr_info.info) (intros_values_eq expr_info []) g)) g
+  else observe_tac (str "equation_others (cont_tac) " ++ Printer.pr_leconstr_env env sigma expr_info.info) (continuation_tac infos) g
 
 let equation_app f_and_args expr_info continuation_tac infos = 
     if expr_info.is_final && expr_info.is_main_branch 
@@ -1417,7 +1419,7 @@ let com_terminate
     nb_args ctx
     hook =
   let start_proof ctx (tac_start:tactic) (tac_end:tactic) =
-    let evd, env = Pfedit.get_current_context () in
+    let evd, env = Pfedit.get_current_context () in (* XXX *)
     Lemmas.start_proof thm_name
       (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
       ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook;
@@ -1469,7 +1471,7 @@ let (com_eqn : int -> Id.t ->
 	| ConstRef c -> is_opaque_constant c
 	| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
     in
-    let evd, env = Pfedit.get_current_context () in
+    let evd, env = Pfedit.get_current_context () in (* XXX *)
     let evd = Evd.from_ctx (Evd.evar_universe_context evd) in
     let f_constr = constr_of_global f_ref in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
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 :
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index ac34faa7da..7db47e13a5 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -877,11 +877,9 @@ struct
     * This is the big generic function for expression parsers.
     *)
 
-  let parse_expr sigma parse_constant parse_exp ops_spec env term =
+  let parse_expr cenv sigma parse_constant parse_exp ops_spec env term =
     if debug
-    then (
-      let _, env = Pfedit.get_current_context () in
-      Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env env sigma term));
+    then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env cenv sigma term);
 
 (*
     let constant_or_variable env term =
@@ -1000,8 +998,7 @@ struct
     |  _ -> raise ParseError
 
 
-  let rconstant sigma term =
-    let _, env = Pfedit.get_current_context () in
+  let rconstant env sigma term =
     if debug
     then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr_env env sigma term ++ fnl ());
     let res = rconstant sigma term in
@@ -1010,7 +1007,7 @@ struct
       res
 
 
-  let parse_zexpr sigma =  parse_expr sigma
+  let parse_zexpr env sigma =  parse_expr env sigma
     (zconstant sigma)
     (fun expr x ->
       let exp = (parse_z sigma x) in
@@ -1019,7 +1016,7 @@ struct
           |   _     ->  Mc.PEpow(expr, Mc.Z.to_N exp))
     zop_spec
 
-  let parse_qexpr sigma =  parse_expr sigma
+  let parse_qexpr env sigma = parse_expr env sigma
    (qconstant sigma)
     (fun expr x ->
       let exp = parse_z sigma x in
@@ -1034,8 +1031,8 @@ struct
                         Mc.PEpow(expr,exp))
    qop_spec
 
-  let parse_rexpr sigma =  parse_expr sigma
-   (rconstant sigma)
+  let parse_rexpr env sigma = parse_expr env sigma
+   (rconstant env sigma)
    (fun expr x ->
       let exp = Mc.N.of_nat (parse_nat sigma x) in
         Mc.PEpow(expr,exp))
@@ -1048,8 +1045,8 @@ struct
     match EConstr.kind sigma cstr with
     | App(op,args) ->
        let (op,lhs,rhs) = parse_op gl (op,args) in
-       let (e1,env) = parse_expr sigma env lhs in
-       let (e2,env) = parse_expr sigma env rhs in
+       let (e1,env) = parse_expr gl.env sigma env lhs in
+       let (e2,env) = parse_expr gl.env sigma env rhs in
         ({Mc.flhs = e1; Mc.fop = op;Mc.frhs = e2},env)
     |  _ -> failwith "error : parse_arith(2)"
 
diff --git a/plugins/setoid_ring/g_newring.mlg b/plugins/setoid_ring/g_newring.mlg
index f59ca4cef4..3ce6478700 100644
--- a/plugins/setoid_ring/g_newring.mlg
+++ b/plugins/setoid_ring/g_newring.mlg
@@ -38,24 +38,24 @@ END
 open Pptactic
 open Ppconstr
 
-let pr_ring_mod = function
-  | Ring_kind (Computational eq_test) -> str "decidable" ++ pr_arg pr_constr_expr eq_test
+let pr_ring_mod env sigma = function
+  | Ring_kind (Computational eq_test) -> str "decidable" ++ pr_arg (pr_constr_expr env sigma) eq_test
   | Ring_kind Abstract ->  str "abstract"
-  | Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg pr_constr_expr morph
-  | Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]"
+  | Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg (pr_constr_expr env sigma) morph
+  | Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma cst_tac ++ str "]"
   | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]"
-  | Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]"
-  | Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]"
-  | Setoid(sth,ext) -> str "setoid" ++ pr_arg pr_constr_expr sth ++ pr_arg pr_constr_expr ext
-  | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]"
-  | Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]"
-  | Sign_spec t -> str "sign" ++ pr_arg pr_constr_expr t
-  | Div_spec t -> str "div" ++ pr_arg pr_constr_expr t
+  | Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma t ++ str "]"
+  | Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma t ++ str "]"
+  | Setoid(sth,ext) -> str "setoid" ++ pr_arg (pr_constr_expr env sigma) sth ++ pr_arg (pr_constr_expr env sigma) ext
+  | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg (pr_constr_expr env sigma) spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]"
+  | Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg (pr_constr_expr env sigma) spec ++ spc () ++ str "[" ++ pr_raw_tactic env sigma cst_tac ++ str "]"
+  | Sign_spec t -> str "sign" ++ pr_arg (pr_constr_expr env sigma) t
+  | Div_spec t -> str "div" ++ pr_arg (pr_constr_expr env sigma) t
 
 }
 
 VERNAC ARGUMENT EXTEND ring_mod
-  PRINTED BY { pr_ring_mod }
+  PRINTED BY { pr_ring_mod env sigma }
   | [ "decidable" constr(eq_test) ] -> { Ring_kind(Computational eq_test) }
   | [ "abstract" ] -> { Ring_kind Abstract }
   | [ "morphism" constr(morph) ] -> { Ring_kind(Morphism morph) }
@@ -74,12 +74,12 @@ END
 
 {
 
-let pr_ring_mods l = surround (prlist_with_sep pr_comma pr_ring_mod l)
+let pr_ring_mods env sigma l = surround (prlist_with_sep pr_comma (pr_ring_mod env sigma) l)
 
 }
 
 VERNAC ARGUMENT EXTEND ring_mods
-  PRINTED BY { pr_ring_mods }
+  PRINTED BY { pr_ring_mods env sigma }
   | [ "(" ne_ring_mod_list_sep(mods, ",") ")" ] -> { mods }
 END
 
@@ -104,26 +104,26 @@ END
 
 {
 
-let pr_field_mod = function
-  | Ring_mod m -> pr_ring_mod m
-  | Inject inj -> str "completeness" ++ pr_arg pr_constr_expr inj
+let pr_field_mod env sigma = function
+  | Ring_mod m -> pr_ring_mod env sigma m
+  | Inject inj -> str "completeness" ++ pr_arg (pr_constr_expr env sigma) inj
 
 }
 
 VERNAC ARGUMENT EXTEND field_mod
-  PRINTED BY { pr_field_mod }
+  PRINTED BY { pr_field_mod env sigma }
   | [ ring_mod(m) ] -> { Ring_mod m }
   | [ "completeness" constr(inj) ] -> { Inject inj }
 END
 
 {
 
-let pr_field_mods l = surround (prlist_with_sep pr_comma pr_field_mod l)
+let pr_field_mods env sigma l = surround (prlist_with_sep pr_comma (pr_field_mod env sigma) l)
 
 }
 
 VERNAC ARGUMENT EXTEND field_mods
-  PRINTED BY { pr_field_mods }
+  PRINTED BY { pr_field_mods env sigma }
   | [ "(" ne_field_mod_list_sep(mods, ",") ")" ] -> { mods }
 END
 
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 58daa7a7d4..6956120a6a 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1232,7 +1232,7 @@ let abs_wgen keep_let f gen (gl,args,c) =
   let evar_closed t p =
     if occur_existential sigma t then
       CErrors.user_err ?loc:(loc_of_cpattern p) ~hdr:"ssreflect"
-        (pr_constr_pat (EConstr.Unsafe.to_constr t) ++
+        (pr_constr_pat env sigma (EConstr.Unsafe.to_constr t) ++
         str" contains holes and matches no subterm of the goal") in
   match gen with
   | _, Some ((x, mode), None) when mode = "@" || (mode = " " && keep_let) ->
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 82a88678f0..3fc05437da 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -133,7 +133,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
   | _ -> false in
   let match_pat env p occ h cl = 
     let sigma0 = project orig_gl in
-    ppdebug(lazy Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern p));
+    ppdebug(lazy Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern env p));
     let (c,ucst), cl =
       fill_occ_pattern ~raise_NoMatch:true env sigma0 (EConstr.Unsafe.to_constr cl) p occ h in
     ppdebug(lazy Pp.(str"     got: " ++ pr_constr_env env sigma0 c));
@@ -239,8 +239,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
       let elimty = Reductionops.whd_all env (project gl) elimty in
       seed, cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl
   in
-  ppdebug(lazy Pp.(str"elim= "++ pr_constr_pat (EConstr.Unsafe.to_constr elim)));
-  ppdebug(lazy Pp.(str"elimty= "++ pr_constr_pat (EConstr.Unsafe.to_constr elimty)));
+  ppdebug(lazy Pp.(str"elim= "++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr elim)));
+  ppdebug(lazy Pp.(str"elimty= "++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr elimty)));
   let inf_deps_r = match EConstr.kind_of_type (project gl) elimty with
     | AtomicType (_, args) -> List.rev (Array.to_list args)
     | _ -> assert false in
@@ -285,8 +285,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
   (* Patterns for the inductive types indexes to be bound in pred are computed
    * looking at the ones provided by the user and the inferred ones looking at
    * the type of the elimination principle *)
-  let pp_pat (_,p,_,occ) = Pp.(pr_occ occ ++ pp_pattern p) in
-  let pp_inf_pat gl (_,_,t,_) = pr_constr_pat (EConstr.Unsafe.to_constr (fire_subst gl t)) in
+  let pp_pat (_,p,_,occ) = Pp.(pr_occ occ ++ pp_pattern env p) in
+  let pp_inf_pat gl (_,_,t,_) = pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr (fire_subst gl t)) in
   let patterns, clr, gl =
     let rec loop patterns clr i = function
       | [],[] -> patterns, clr, gl
@@ -300,7 +300,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
           loop (patterns @ [i, p, inf_t, occ]) 
             (clr_t @ clr) (i+1) (deps, inf_deps)
       | [], c :: inf_deps -> 
-          ppdebug(lazy Pp.(str"adding inf pattern " ++ pr_constr_pat (EConstr.Unsafe.to_constr c)));
+          ppdebug(lazy Pp.(str"adding inf pattern " ++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr c)));
           loop (patterns @ [i, mkTpat gl c, c, allocc]) 
             clr (i+1) ([], inf_deps)
       | _::_, [] -> errorstrm Pp.(str "Too many dependent abstractions") in
@@ -323,11 +323,11 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
   let elim_pred, gen_eq_tac, clr, gl = 
     let error gl t inf_t = errorstrm Pp.(str"The given pattern matches the term"++
       spc()++pp_term gl t++spc()++str"while the inferred pattern"++
-      spc()++pr_constr_pat (EConstr.Unsafe.to_constr (fire_subst gl inf_t))++spc()++ str"doesn't") in
+      spc()++pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr (fire_subst gl inf_t))++spc()++ str"doesn't") in
     let match_or_postpone (cl, gl, post) (h, p, inf_t, occ) =
       let p = unif_redex gl p inf_t in
       if is_undef_pat p then
-        let () = ppdebug(lazy Pp.(str"postponing " ++ pp_pattern p)) in
+        let () = ppdebug(lazy Pp.(str"postponing " ++ pp_pattern env p)) in
         cl, gl, post @ [h, p, inf_t, occ]
       else try
         let c, cl, ucst = match_pat env p occ h cl in
@@ -408,7 +408,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
     if not (Evar.Set.is_empty inter) then begin
       let i = Evar.Set.choose inter in
       let pat = List.find (fun t -> Evar.Set.mem i (evars_of_term t)) patterns in
-      errorstrm Pp.(str"Pattern"++spc()++pr_constr_pat (EConstr.Unsafe.to_constr pat)++spc()++
+      errorstrm Pp.(str"Pattern"++spc()++pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr pat)++spc()++
         str"was not completely instantiated and one of its variables"++spc()++
         str"occurs in the type of another non-instantiated pattern variable");
     end
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 18461c0533..15480c7a45 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -199,13 +199,13 @@ let simplintac occ rdx sim gl =
   | SimplCut (n,m) -> tclTHEN (simptac m) (tclTRY (donetac n)) gl
   | _ -> simpltac sim gl
 
-let rec get_evalref sigma c = match EConstr.kind sigma c with
+let rec get_evalref env sigma c = match EConstr.kind sigma c with
   | Var id -> EvalVarRef id
   | Const (k,_) -> EvalConstRef k
-  | App (c', _) -> get_evalref sigma c'
-  | Cast (c', _, _) -> get_evalref sigma c'
+  | App (c', _) -> get_evalref env sigma c'
+  | Cast (c', _, _) -> get_evalref env sigma c'
   | Proj(c,_) -> EvalConstRef(Projection.constant c)
-  | _ -> errorstrm Pp.(str "The term " ++ pr_constr_pat (EConstr.Unsafe.to_constr c) ++ str " is not unfoldable")
+  | _ -> errorstrm Pp.(str "The term " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr c) ++ str " is not unfoldable")
 
 (* Strip a pattern generated by a prenex implicit to its constant. *)
 let strip_unfold_term _ ((sigma, t) as p) kt = match EConstr.kind sigma t with
@@ -230,7 +230,7 @@ let unfoldintac occ rdx t (kt,_) gl =
   let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
   let (sigma, t), const = strip_unfold_term env0 t kt in
   let body env t c =
-    Tacred.unfoldn [AllOccurrences, get_evalref sigma t] env sigma0 c in
+    Tacred.unfoldn [AllOccurrences, get_evalref env sigma t] env sigma0 c in
   let easy = occ = None && rdx = None in
   let red_flags = if easy then CClosure.betaiotazeta else CClosure.betaiota in
   let beta env = Reductionops.clos_norm_flags red_flags env sigma0 in
@@ -244,7 +244,7 @@ let unfoldintac occ rdx t (kt,_) gl =
       try find_T env c h ~k:(fun env c _ _ -> EConstr.Unsafe.to_constr (body env t (EConstr.of_constr c)))
       with NoMatch when easy -> c
       | NoMatch | NoProgress -> errorstrm Pp.(str"No occurrence of "
-        ++ pr_constr_pat (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr_env env sigma c)),
+        ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr_env env sigma c)),
     (fun () -> try end_T () with 
       | NoMatch when easy -> fake_pmatcher_end () 
       | NoMatch -> anomaly "unfoldintac")
@@ -270,12 +270,12 @@ let unfoldintac occ rdx t (kt,_) gl =
       else
         try EConstr.Unsafe.to_constr @@ body env t (fs (unify_HO env sigma (EConstr.of_constr c) t) t)
         with _ -> errorstrm Pp.(str "The term " ++
-          pr_constr_env env sigma c ++spc()++ str "does not unify with " ++ pr_constr_pat (EConstr.Unsafe.to_constr t))),
+          pr_constr_env env sigma c ++spc()++ str "does not unify with " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr t))),
     fake_pmatcher_end in
   let concl = 
     let concl0 = EConstr.Unsafe.to_constr concl0 in
     try beta env0 (EConstr.of_constr (eval_pattern env0 sigma0 concl0 rdx occ unfold)) 
-    with Option.IsNone -> errorstrm Pp.(str"Failed to unfold " ++ pr_constr_pat (EConstr.Unsafe.to_constr t)) in
+    with Option.IsNone -> errorstrm Pp.(str"Failed to unfold " ++ pr_constr_pat env0 sigma (EConstr.Unsafe.to_constr t)) in
   let _ = conclude () in
   Proofview.V82.of_tactic (convert_concl concl) gl
 ;;
@@ -298,8 +298,8 @@ let foldtac occ rdx ft gl =
        try
          let sigma = unify_HO env sigma (EConstr.of_constr c) (EConstr.of_constr t) in
          EConstr.to_constr ~abort_on_undefined_evars:false sigma (EConstr.of_constr t)
-    with _ -> errorstrm Pp.(str "fold pattern " ++ pr_constr_pat t ++ spc ()
-      ++ str "does not match redex " ++ pr_constr_pat c)), 
+    with _ -> errorstrm Pp.(str "fold pattern " ++ pr_constr_pat env sigma t ++ spc ()
+      ++ str "does not match redex " ++ pr_constr_pat env sigma c)),
     fake_pmatcher_end in
   let concl0 = EConstr.Unsafe.to_constr concl0 in
   let concl = eval_pattern env0 sigma0 concl0 rdx occ fold in
@@ -412,7 +412,7 @@ let rwcltac cl rdx dir sr gl =
       let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in
       let r3, _, r3t  = 
         try EConstr.destCast (project gl) r2 with _ ->
-        errorstrm Pp.(str "no cast from " ++ pr_constr_pat (EConstr.Unsafe.to_constr (snd sr))
+        errorstrm Pp.(str "no cast from " ++ pr_constr_pat (pf_env gl) (project gl) (EConstr.Unsafe.to_constr (snd sr))
                     ++ str " to " ++ pr_econstr_env (pf_env gl) (project gl) r2) in
       let cl' = EConstr.mkNamedProd (make_annot rule_id Sorts.Relevant) (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in
       let cl'' = EConstr.mkNamedProd (make_annot pattern_id Sorts.Relevant) rdxt cl' in
@@ -473,7 +473,7 @@ let rwprocess_rule dir rule gl =
       let t =
         if red = 1 then Tacred.hnf_constr env sigma t0
         else Reductionops.whd_betaiotazeta sigma t0 in
-      ppdebug(lazy Pp.(str"rewrule="++pr_constr_pat (EConstr.Unsafe.to_constr t)));
+      ppdebug(lazy Pp.(str"rewrule="++pr_constr_pat env sigma (EConstr.Unsafe.to_constr t)));
       match EConstr.kind sigma t with
       | Prod (_, xt, at) ->
         let sigma = Evd.create_evar_defs sigma in
@@ -532,8 +532,8 @@ let rwprocess_rule dir rule gl =
         sigma, (d, r', lhs, rhs) :: rs
       | _ ->
         if red = 0 then loop d sigma r t rs 1
-        else errorstrm Pp.(str "not a rewritable relation: " ++ pr_constr_pat (EConstr.Unsafe.to_constr t)
-                        ++ spc() ++ str "in rule " ++ pr_constr_pat  (EConstr.Unsafe.to_constr (snd rule)))
+        else errorstrm Pp.(str "not a rewritable relation: " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr t)
+                        ++ spc() ++ str "in rule " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr (snd rule)))
         in
     let sigma, r = rule in
     let t = Retyping.get_type_of env sigma r in
@@ -547,9 +547,9 @@ let rwrxtac occ rdx_pat dir rule gl =
   let find_rule rdx =
     let rec rwtac = function
       | [] ->
-        errorstrm Pp.(str "pattern " ++ pr_constr_pat (EConstr.Unsafe.to_constr rdx) ++
+        errorstrm Pp.(str "pattern " ++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr rdx) ++
                    str " does not match " ++ pr_dir_side dir ++
-                   str " of " ++ pr_constr_pat (EConstr.Unsafe.to_constr (snd rule)))
+                   str " of " ++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr (snd rule)))
       | (d, r, lhs, rhs) :: rs ->
         try
           let ise = unify_HO env (Evd.create_evar_defs r_sigma) lhs rdx in
@@ -640,7 +640,7 @@ let ssrrewritetac ist rwargs =
 let unfoldtac occ ko t kt gl =
   let env = pf_env gl in
   let cl, c = pf_fill_occ_term gl occ (fst (strip_unfold_term env t kt)) in
-  let cl' = EConstr.Vars.subst1 (pf_unfoldn [OnlyOccurrences [1], get_evalref (project gl) c] gl c) cl in
+  let cl' = EConstr.Vars.subst1 (pf_unfoldn [OnlyOccurrences [1], get_evalref env (project gl) c] gl c) cl in
   let f = if ko = None then CClosure.betaiotazeta else CClosure.betaiota in
   Proofview.V82.of_tactic
     (convert_concl (pf_reduce (Reductionops.clos_norm_flags f) gl cl')) gl
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 9ea35b8694..be9586fdd7 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -50,7 +50,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl =
   let c = EConstr.of_constr c in
   let cl = EConstr.of_constr cl in
   if Termops.occur_existential sigma c then errorstrm(str"The pattern"++spc()++
-    pr_constr_pat (EConstr.Unsafe.to_constr c)++spc()++str"did not match and has holes."++spc()++
+    pr_constr_pat env sigma (EConstr.Unsafe.to_constr c)++spc()++str"did not match and has holes."++spc()++
     str"Did you mean pose?") else
   let c, (gl, cty) =  match EConstr.kind sigma c with
   | Cast(t, DEFAULTcast, ty) -> t, (gl, ty)
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 2a2cd73df2..0ec5f1673a 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -74,11 +74,11 @@ let frozen_lexer = CLexer.get_keyword_state () ;;
 
 let tacltop = (5,Notation_gram.E)
 
-let pr_ssrtacarg _ _ prt = prt tacltop
+let pr_ssrtacarg env sigma _ _ prt = prt env sigma tacltop
 
 }
 
-ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY { pr_ssrtacarg }
+ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma }
 | [ "YouShouldNotTypeThis" ] -> { CErrors.anomaly (Pp.str "Grammar placeholder match") }
 END
 GRAMMAR EXTEND Gram
@@ -89,12 +89,12 @@ END
 {
 
 (* Lexically closed tactic for tacticals. *)
-let pr_ssrtclarg _ _ prt tac = prt tacltop tac
+let pr_ssrtclarg env sigma _ _ prt tac = prt env sigma tacltop tac
 
 }
 
 ARGUMENT EXTEND ssrtclarg TYPED AS ssrtacarg
-    PRINTED BY { pr_ssrtclarg }
+    PRINTED BY { pr_ssrtclarg env sigma }
 | [ ssrtacarg(tac) ] -> { tac }
 END
 
@@ -109,7 +109,7 @@ let add_genarg tag pr =
   let glob ist x = (ist, x) in
   let subst _ x = x in
   let interp ist x = Ftactic.return (Geninterp.Val.Dyn (tag, x)) in
-  let gen_pr _ _ _ = pr in
+  let gen_pr env sigma _ _ _ = pr env sigma in
   let () = Genintern.register_intern0 wit glob in
   let () = Genintern.register_subst0 wit subst in
   let () = Geninterp.register_interp0 wit interp in
@@ -146,7 +146,7 @@ let pr_list = prlist_with_sep
 
 let pr_ssrhyp _ _ _ = pr_hyp
 
-let wit_ssrhyprep = add_genarg "ssrhyprep" pr_hyp
+let wit_ssrhyprep = add_genarg "ssrhyprep" (fun env sigma -> pr_hyp)
 
 let intern_hyp ist (SsrHyp (loc, id) as hyp) =
   let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) CAst.(make ?loc id)) in
@@ -168,7 +168,7 @@ END
 let pr_hoi = hoik pr_hyp
 let pr_ssrhoi _ _ _ = pr_hoi
 
-let wit_ssrhoirep = add_genarg "ssrhoirep" pr_hoi
+let wit_ssrhoirep = add_genarg "ssrhoirep" (fun env sigma -> pr_hoi)
 
 let intern_ssrhoi ist = function
   | Hyp h -> Hyp (intern_hyp ist h)
@@ -212,13 +212,13 @@ END
 
 let pr_rwdir = function L2R -> mt() | R2L -> str "-"
 
-let wit_ssrdir = add_genarg "ssrdir" pr_dir
+let wit_ssrdir = add_genarg "ssrdir" (fun env sigma -> pr_dir)
 
 (** Simpl switch *)
 
 let pr_ssrsimpl _ _ _ = pr_simpl
 
-let wit_ssrsimplrep = add_genarg "ssrsimplrep" pr_simpl
+let wit_ssrsimplrep = add_genarg "ssrsimplrep" (fun env sigma -> pr_simpl)
 
 let test_ssrslashnum b1 b2 strm =
   match Util.stream_nth 0 strm with
@@ -413,7 +413,7 @@ END
 
 let pr_mmod = function May -> str "?" | Must -> str "!" | Once -> mt ()
 
-let wit_ssrmmod = add_genarg "ssrmmod" pr_mmod
+let wit_ssrmmod = add_genarg "ssrmmod" (fun env sigma -> pr_mmod)
 let ssrmmod = Pcoq.create_generic_entry Pcoq.utactic "ssrmmod" (Genarg.rawwit wit_ssrmmod);;
 
 }
@@ -643,7 +643,7 @@ and map_block map_id = function
   | SuffixNum _ as x -> x
 
 type ssripatrep = ssripat
-let wit_ssripatrep = add_genarg "ssripatrep" pr_ipat
+let wit_ssripatrep = add_genarg "ssripatrep" (fun env sigma -> pr_ipat)
 
 let pr_ssripat _ _ _ = pr_ipat
 let pr_ssripats _ _ _ = pr_ipats
@@ -950,13 +950,13 @@ END
 
 {
 
-let pr_ssrintrosarg _ _ prt (tac, ipats) =
-  prt tacltop tac ++ pr_intros spc ipats
+let pr_ssrintrosarg env sigma _ _ prt (tac, ipats) =
+  prt env sigma tacltop tac ++ pr_intros spc ipats
 
 }
 
 ARGUMENT EXTEND ssrintrosarg TYPED AS (tactic * ssrintros)
-   PRINTED BY { pr_ssrintrosarg }
+   PRINTED BY { pr_ssrintrosarg env sigma }
 | [ "YouShouldNotTypeThis" ssrtacarg(arg) ssrintros_ne(ipats) ] -> { arg, ipats }
 END
 
@@ -1007,22 +1007,22 @@ GRAMMAR EXTEND Gram
 
 {
 
-let pr_ortacs prt = 
+let pr_ortacs env sigma prt =
   let rec pr_rec = function
   | [None]           -> spc() ++ str "|" ++ spc()
   | None :: tacs     -> spc() ++ str "|" ++ pr_rec tacs
-  | Some tac :: tacs -> spc() ++ str "| " ++ prt tacltop tac ++  pr_rec tacs
+  | Some tac :: tacs -> spc() ++ str "| " ++ prt env sigma tacltop tac ++  pr_rec tacs
   | []                -> mt() in
   function
   | [None]           -> spc()
   | None :: tacs     -> pr_rec tacs
-  | Some tac :: tacs -> prt tacltop tac ++ pr_rec tacs
+  | Some tac :: tacs -> prt env sigma tacltop tac ++ pr_rec tacs
   | []                -> mt()
-let pr_ssrortacs _ _ = pr_ortacs
+let pr_ssrortacs env sigma _ _ = pr_ortacs env sigma
 
 }
 
-ARGUMENT EXTEND ssrortacs TYPED AS tactic option list PRINTED BY { pr_ssrortacs }
+ARGUMENT EXTEND ssrortacs TYPED AS tactic option list PRINTED BY { pr_ssrortacs env sigma }
 | [ ssrtacarg(tac) "|" ssrortacs(tacs) ] -> { Some tac :: tacs }
 | [ ssrtacarg(tac) "|" ] -> { [Some tac; None] }
 | [ ssrtacarg(tac) ] -> { [Some tac] }
@@ -1032,34 +1032,34 @@ END
 
 {
 
-let pr_hintarg prt = function
-  | true, tacs -> hv 0 (str "[ " ++ pr_ortacs prt tacs ++ str " ]")
-  | false, [Some tac] -> prt tacltop tac
+let pr_hintarg env sigma prt = function
+  | true, tacs -> hv 0 (str "[ " ++ pr_ortacs env sigma prt tacs ++ str " ]")
+  | false, [Some tac] -> prt env sigma tacltop tac
   | _, _ -> mt()
 
-let pr_ssrhintarg _ _ = pr_hintarg
+let pr_ssrhintarg env sigma _ _ = pr_hintarg env sigma
 
 }
 
-ARGUMENT EXTEND ssrhintarg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintarg }
+ARGUMENT EXTEND ssrhintarg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintarg env sigma }
 | [ "[" "]" ] -> { nullhint }
 | [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs }
 | [ ssrtacarg(arg) ] -> { mk_hint arg }
 END
 
-ARGUMENT EXTEND ssrortacarg TYPED AS ssrhintarg PRINTED BY { pr_ssrhintarg }
+ARGUMENT EXTEND ssrortacarg TYPED AS ssrhintarg PRINTED BY { pr_ssrhintarg env sigma }
 | [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs }
 END
 
 {
 
-let pr_hint prt arg =
-  if arg = nohint then mt() else str "by " ++ pr_hintarg prt arg
-let pr_ssrhint _ _ = pr_hint
+let pr_hint env sigma prt arg =
+  if arg = nohint then mt() else str "by " ++ pr_hintarg env sigma prt arg
+let pr_ssrhint env sigma _ _ = pr_hint env sigma
 
 }
 
-ARGUMENT EXTEND ssrhint TYPED AS ssrhintarg PRINTED BY { pr_ssrhint }
+ARGUMENT EXTEND ssrhint TYPED AS ssrhintarg PRINTED BY { pr_ssrhint env sigma }
 | [ ]                       -> { nohint }
 END
 (** The "in" pseudo-tactical *)
@@ -1117,7 +1117,7 @@ let pr_clseq = function
   | InHypsSeq       -> str " |-"
   | InAllHyps       -> str "* |-"
 
-let wit_ssrclseq = add_genarg "ssrclseq" pr_clseq
+let wit_ssrclseq = add_genarg "ssrclseq" (fun env sigma -> pr_clseq)
 let pr_clausehyps = pr_list pr_spc pr_wgen
 let pr_ssrclausehyps _ _ _ = pr_clausehyps
 
@@ -1220,7 +1220,7 @@ let pr_fwdkind = function
   | FwdHint (s,_) -> str (s ^ " ") | _ -> str " :=" ++ spc ()
 let pr_fwdfmt (fk, _ : ssrfwdfmt) = pr_fwdkind fk
 
-let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" pr_fwdfmt
+let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" (fun env sigma -> pr_fwdfmt)
 
 (* type ssrfwd = ssrfwdfmt * ssrterm *)
 
@@ -1283,11 +1283,11 @@ END
 
 {
 
-let pr_ssrbvar prc _ _ v = prc v
+let pr_ssrbvar env sigma prc _ _ v = prc env sigma v
 
 }
 
-ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY { pr_ssrbvar }
+ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY { pr_ssrbvar env sigma }
 | [ ident(id) ] -> { mkCVar ~loc id }
 | [ "_" ] -> { mkCHole (Some loc) }
 END
@@ -1299,11 +1299,11 @@ let bvar_lname = let open CAst in function
     CAst.make ?loc:qid.CAst.loc @@ Name (qualid_basename qid)
   | { loc = loc } -> CAst.make ?loc Anonymous
 
-let pr_ssrbinder prc _ _ (_, c) = prc c
+let pr_ssrbinder env sigma prc _ _ (_, c) = prc env sigma c
 
 }
 
-ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinder }
+ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinder env sigma }
  | [ ssrbvar(bv) ] ->
    { let { CAst.loc=xloc } as x = bvar_lname bv in
      (FwdPose, [BFvar]),
@@ -1474,11 +1474,11 @@ END
 
 {
 
-let pr_ssrhavefwd _ _ prt (fwd, hint) = pr_fwd fwd ++ pr_hint prt hint
+let pr_ssrhavefwd env sigma _ _ prt (fwd, hint) = pr_fwd fwd ++ pr_hint env sigma prt hint
 
 }
 
-ARGUMENT EXTEND ssrhavefwd TYPED AS (ssrfwd * ssrhint) PRINTED BY { pr_ssrhavefwd }
+ARGUMENT EXTEND ssrhavefwd TYPED AS (ssrfwd * ssrhint) PRINTED BY { pr_ssrhavefwd env sigma }
 | [ ":" ast_closure_lterm(t) ssrhint(hint) ] -> { mkFwdHint ":" t, hint }
 | [ ":" ast_closure_lterm(t) ":=" ast_closure_lterm(c) ] -> { mkFwdCast FwdHave ~loc t ~c, nohint }
 | [ ":" ast_closure_lterm(t) ":=" ] -> { mkFwdHintNoTC ":" t, nohint }
@@ -1503,14 +1503,14 @@ let binder_to_intro_id = CAst.(List.map (function
   | (FwdPose, [BFdef]), { v = CLetIn ({v=Anonymous},_,_,_) } -> [IPatAnon (One None)]
   | _ -> anomaly "ssrbinder is not a binder"))
 
-let pr_ssrhavefwdwbinders _ _ prt (tr,((hpats, (fwd, hint)))) =
-  pr_hpats hpats ++ pr_fwd fwd ++ pr_hint prt hint
+let pr_ssrhavefwdwbinders env sigma _ _ prt (tr,((hpats, (fwd, hint)))) =
+  pr_hpats hpats ++ pr_fwd fwd ++ pr_hint env sigma prt hint
 
 }
 
 ARGUMENT EXTEND ssrhavefwdwbinders
   TYPED AS (bool * (ssrhpats * (ssrfwd * ssrhint)))
-  PRINTED BY { pr_ssrhavefwdwbinders }
+  PRINTED BY { pr_ssrhavefwdwbinders env sigma }
 | [ ssrhpats_wtransp(trpats) ssrbinder_list(bs) ssrhavefwd(fwd) ] ->
   { let tr, pats = trpats in
     let ((clr, pats), binders), simpl = pats in
@@ -1522,14 +1522,14 @@ END
 
 {
 
-let pr_ssrdoarg prc _ prt (((n, m), tac), clauses) =
-  pr_index n ++ pr_mmod m ++ pr_hintarg prt tac ++ pr_clauses clauses
+let pr_ssrdoarg env sigma prc _ prt (((n, m), tac), clauses) =
+  pr_index n ++ pr_mmod m ++ pr_hintarg env sigma prt tac ++ pr_clauses clauses
 
 }
 
 ARGUMENT EXTEND ssrdoarg
   TYPED AS (((ssrindex * ssrmmod) * ssrhintarg) * ssrclauses)
-  PRINTED BY { pr_ssrdoarg }
+  PRINTED BY { pr_ssrdoarg env sigma }
 | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" }
 END
 
@@ -1537,22 +1537,22 @@ END
 
 (* type ssrseqarg = ssrindex * (ssrtacarg * ssrtac option) *)
 
-let pr_seqtacarg prt = function
+let pr_seqtacarg env sigma prt = function
   | (is_first, []), _ -> str (if is_first then "first" else "last")
   | tac, Some dtac ->
-    hv 0 (pr_hintarg prt tac ++ spc() ++ str "|| " ++ prt tacltop dtac)
-  | tac, _ -> pr_hintarg prt tac
+    hv 0 (pr_hintarg env sigma prt tac ++ spc() ++ str "|| " ++ prt env sigma tacltop dtac)
+  | tac, _ -> pr_hintarg env sigma prt tac
 
-let pr_ssrseqarg _ _ prt = function
-  | ArgArg 0, tac -> pr_seqtacarg prt tac
-  | i, tac -> pr_index i ++ str " " ++ pr_seqtacarg prt tac
+let pr_ssrseqarg env sigma _ _ prt = function
+  | ArgArg 0, tac -> pr_seqtacarg env sigma prt tac
+  | i, tac -> pr_index i ++ str " " ++ pr_seqtacarg env sigma prt tac
 
 }
 
 (* We must parse the index separately to resolve the conflict with *)
 (* an unindexed tactic.                                            *)
 ARGUMENT EXTEND ssrseqarg TYPED AS (ssrindex * (ssrhintarg * tactic option))
-                          PRINTED BY { pr_ssrseqarg }
+                          PRINTED BY { pr_ssrseqarg env sigma }
 | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" }
 END
 
@@ -2278,7 +2278,7 @@ let pr_rwkind = function
   | RWdef -> str "/"
   | RWeq -> mt ()
 
-let wit_ssrrwkind = add_genarg "ssrrwkind" pr_rwkind
+let wit_ssrrwkind = add_genarg "ssrrwkind" (fun env sigma -> pr_rwkind)
 
 let pr_rule = function
   | RWred s, _ -> pr_simpl s
@@ -2520,13 +2520,13 @@ END
 
 {
 
-let pr_ssrsufffwdwbinders _ _ prt (hpats, (fwd, hint)) =
-  pr_hpats hpats ++ pr_fwd fwd ++ pr_hint prt hint
+let pr_ssrsufffwdwbinders env sigma _ _ prt (hpats, (fwd, hint)) =
+  pr_hpats hpats ++ pr_fwd fwd ++ pr_hint env sigma prt hint
 
 }
 
 ARGUMENT EXTEND ssrsufffwd
-  TYPED AS (ssrhpats * (ssrfwd * ssrhint)) PRINTED BY { pr_ssrsufffwdwbinders }
+  TYPED AS (ssrhpats * (ssrfwd * ssrhint)) PRINTED BY { pr_ssrsufffwdwbinders env sigma }
 | [ ssrhpats(pats) ssrbinder_list(bs)  ":" ast_closure_lterm(t) ssrhint(hint) ] ->
   { let ((clr, pats), binders), simpl = pats in
     let allbs = intro_id_to_binder binders @ bs in
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index 7844050272..4a872be6a5 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -14,13 +14,15 @@ 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 : 'a -> 'b -> (Notation_gram.tolerability -> 'c) -> 'c
+val pr_ssrtacarg : Environ.env -> Evd.evar_map -> 'a -> 'b ->
+  (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> '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 : 'a -> 'b -> (Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd
+val pr_ssrtclarg : Environ.env -> Evd.evar_map -> 'a -> 'b ->
+  (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd
 
-val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type
+val add_genarg : string -> (Environ.env -> Evd.evar_map -> 'a -> Pp.t) -> 'a Genarg.uniform_genarg_type
 
 (* Parsing witnesses, needed to serialize ssreflect syntax *)
 open Ssrmatching_plugin
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index 38f5b7d107..5d8c94e49b 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -57,11 +57,17 @@ let pr_guarded guard prc c =
   let s = Format.flush_str_formatter () ^ "$" in
   if guard s (skip_wschars s 0) then pr_paren prc c else prc c
 
-let prl_constr_expr = Ppconstr.pr_lconstr_expr
+let prl_constr_expr =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  Ppconstr.pr_lconstr_expr env sigma
 let pr_glob_constr c = Printer.pr_glob_constr_env (Global.env ()) c
 let prl_glob_constr c = Printer.pr_lglob_constr_env (Global.env ()) c
 let pr_glob_constr_and_expr = function
-  | _, Some c -> Ppconstr.pr_constr_expr c
+  | _, Some c ->
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    Ppconstr.pr_constr_expr env sigma c
   | c, None -> pr_glob_constr c
 let pr_term (k, c) = pr_guarded (guard_term k) pr_glob_constr_and_expr c
 
@@ -91,7 +97,10 @@ let pr_simpl = function
 
 (* New terms *)
 
-let pr_ast_closure_term { body } = Ppconstr.pr_constr_expr body
+let pr_ast_closure_term { body } =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  Ppconstr.pr_constr_expr env sigma body
 
 let pr_view2 = pr_list mt (fun c -> str "/" ++ pr_ast_closure_term c)
 
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 2e1554d496..d3f89147fa 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -198,13 +198,13 @@ type raw_glob_search_about_item =
   | RGlobSearchSubPattern of constr_expr
   | RGlobSearchString of Loc.t * string * string option
 
-let pr_search_item = function
+let pr_search_item env sigma = function
   | RGlobSearchString (_,s,_) -> str s
-  | RGlobSearchSubPattern p -> pr_constr_expr p
+  | RGlobSearchSubPattern p -> pr_constr_expr env sigma p
 
 let wit_ssr_searchitem = add_genarg "ssr_searchitem" pr_search_item
 
-let pr_ssr_search_item _ _ _ = pr_search_item
+let pr_ssr_search_item env sigma _ _ _ = pr_search_item env sigma
 
 (* Workaround the notation API that can only print notations *)
 
@@ -316,7 +316,7 @@ let interp_search_notation ?loc tag okey =
 }
 
 ARGUMENT EXTEND ssr_search_item TYPED AS ssr_searchitem
-  PRINTED BY { pr_ssr_search_item }
+  PRINTED BY { pr_ssr_search_item env sigma }
   | [ string(s) ] -> {  RGlobSearchString (loc,s,None)  }
   | [ string(s) "%" preident(key) ] -> {  RGlobSearchString (loc,s,Some key)  }
   | [ constr_pattern(p) ] -> {  RGlobSearchSubPattern p  }
@@ -324,14 +324,14 @@ END
 
 {
 
-let pr_ssr_search_arg _ _ _ =
-  let pr_item (b, p) = str (if b then "-" else "") ++ pr_search_item p in
+let pr_ssr_search_arg env sigma _ _ _ =
+  let pr_item (b, p) = str (if b then "-" else "") ++ pr_search_item env sigma p in
   pr_list spc pr_item
 
 }
 
 ARGUMENT EXTEND ssr_search_arg TYPED AS (bool * ssr_searchitem) list
-  PRINTED BY { pr_ssr_search_arg }
+  PRINTED BY { pr_ssr_search_arg env sigma }
   | [ "-" ssr_search_item(p) ssr_search_arg(a) ] -> {  (false, p) :: a  }
   | [ ssr_search_item(p) ssr_search_arg(a) ] -> {  (true, p) :: a  }
   | [ ] -> {  []  }
@@ -432,7 +432,7 @@ let interp_search_arg arg =
 
 let pr_modloc (b, m) = if b then str "-" ++ pr_qualid m else pr_qualid m
 
-let wit_ssrmodloc = add_genarg "ssrmodloc" pr_modloc
+let wit_ssrmodloc = add_genarg "ssrmodloc" (fun env sigma -> pr_modloc)
 
 let pr_ssr_modlocs _ _ _ ml =
   if ml = [] then str "" else spc () ++ str "in " ++ pr_list spc pr_modloc ml
@@ -491,24 +491,23 @@ END
 
 {
 
-let pr_raw_ssrhintref prc _ _ = let open CAst in function
+let pr_raw_ssrhintref env sigma prc _ _ = let open CAst in function
   | { v = CAppExpl ((None, r,x), args) } when isCHoles args ->
-    prc (CAst.make @@ CRef (r,x)) ++ str "|" ++ int (List.length args)
-  | { v = CApp ((_, { v = CRef _ }), _) } as c -> prc c
+    prc env sigma (CAst.make @@ CRef (r,x)) ++ str "|" ++ int (List.length args)
+  | { v = CApp ((_, { v = CRef _ }), _) } as c -> prc env sigma c
   | { v = CApp ((_, c), args) } when isCxHoles args ->
-    prc c ++ str "|" ++ int (List.length args)
-  | c -> prc c
+    prc env sigma c ++ str "|" ++ int (List.length args)
+  | c -> prc env sigma c
 
-let pr_rawhintref c =
-  let _, env = Pfedit.get_current_context () in
+let pr_rawhintref env sigma c =
   match DAst.get c with
   | GApp (f, args) when isRHoles args ->
     pr_glob_constr_env env f ++ str "|" ++ int (List.length args)
   | _ -> pr_glob_constr_env env c
 
-let pr_glob_ssrhintref _ _ _ (c, _) = pr_rawhintref c
+let pr_glob_ssrhintref env sigma _ _ _ (c, _) = pr_rawhintref env sigma c
 
-let pr_ssrhintref prc _ _ = prc
+let pr_ssrhintref env sigma prc _ _ = prc env sigma
 
 let mkhintref ?loc c n = match c.CAst.v with
   | CRef (r,x) -> CAst.make ?loc @@ CAppExpl ((None, r, x), mkCHoles ?loc n)
@@ -518,9 +517,9 @@ let mkhintref ?loc c n = match c.CAst.v with
 
 ARGUMENT EXTEND ssrhintref
   TYPED AS constr
-  PRINTED BY { pr_ssrhintref }
-  RAW_PRINTED BY { pr_raw_ssrhintref }
-  GLOB_PRINTED BY { pr_glob_ssrhintref }
+  PRINTED BY { pr_ssrhintref env sigma }
+  RAW_PRINTED BY { pr_raw_ssrhintref env sigma }
+  GLOB_PRINTED BY { pr_glob_ssrhintref env sigma }
   | [ constr(c) ] -> {  c  }
   | [ constr(c) "|" natural(n) ] -> {  mkhintref ~loc c n  }
 END
@@ -559,19 +558,22 @@ END
 
 {
 
-let print_view_hints kind l =
+let print_view_hints env sigma kind l =
   let pp_viewname = str "Hint View" ++ pr_viewpos (Some kind) ++ str " " in
-  let pp_hints = pr_list spc pr_rawhintref l in
+  let pp_hints = pr_list spc (pr_rawhintref env sigma) l in
   Feedback.msg_info  (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ())
 
 }
 
 VERNAC COMMAND EXTEND PrintView CLASSIFIED AS QUERY
 | [ "Print" "Hint" "View" ssrviewpos(i) ] ->
-  { match i with
-    | Some k -> print_view_hints k (Ssrview.AdaptorDb.get k)
+  {
+    let sigma, env = Pfedit.get_current_context () in
+    match i with
+    | Some k ->
+      print_view_hints env sigma k (Ssrview.AdaptorDb.get k)
     | None ->
-        List.iter (fun k -> print_view_hints k (Ssrview.AdaptorDb.get k))
+        List.iter (fun k -> print_view_hints env sigma k (Ssrview.AdaptorDb.get k))
           [ Ssrview.AdaptorDb.Forward;
             Ssrview.AdaptorDb.Backward;
             Ssrview.AdaptorDb.Equivalence ]
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index b83a6a34cb..5eb106cc26 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -97,14 +97,20 @@ let prl_glob_constr c = pr_lglob_constr_env (Global.env ()) c
 let pr_glob_constr c = pr_glob_constr_env (Global.env ()) c
 let prl_constr_expr = pr_lconstr_expr
 let pr_constr_expr = pr_constr_expr
-let prl_glob_constr_and_expr = function
-  | _, Some c -> prl_constr_expr c
+let prl_glob_constr_and_expr env sigma = function
+  | _, Some c -> prl_constr_expr env sigma c
   | c, None -> prl_glob_constr c
-let pr_glob_constr_and_expr = function
-  | _, Some c -> pr_constr_expr c
+let pr_glob_constr_and_expr env sigma = function
+  | _, Some c -> pr_constr_expr env sigma c
   | c, None -> pr_glob_constr c
-let pr_term (k, c, _) = pr_guarded (guard_term k) pr_glob_constr_and_expr c
-let prl_term (k, c, _) = pr_guarded (guard_term k) prl_glob_constr_and_expr c
+let pr_term (k, c, _) =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  pr_guarded (guard_term k) (pr_glob_constr_and_expr env sigma) c
+let prl_term (k, c, _) =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  pr_guarded (guard_term k) (prl_glob_constr_and_expr env sigma) c
 
 (** Adding a new uninterpreted generic argument type *)
 let add_genarg tag pr =
@@ -113,7 +119,7 @@ let add_genarg tag pr =
   let glob ist x = (ist, x) in
   let subst _ x = x in
   let interp ist x = Ftactic.return (Geninterp.Val.Dyn (tag, x)) in
-  let gen_pr _ _ _ = pr in
+  let gen_pr env sigma _ _ _ = pr env sigma in
   let () = Genintern.register_intern0 wit glob in
   let () = Genintern.register_subst0 wit subst in
   let () = Geninterp.register_interp0 wit interp in
@@ -362,10 +368,9 @@ let isRigid c = match kind c with
   | _ -> false
 
 let hole_var = mkVar (Id.of_string "_")
-let pr_constr_pat c0 =
+let pr_constr_pat env sigma c0 =
   let rec wipe_evar c =
     if isEvar c then hole_var else map wipe_evar c in
-  let sigma, env = Pfedit.get_current_context () in
   pr_constr_env env sigma (wipe_evar c0)
 
 (* Turn (new) evars into metas *)
@@ -417,7 +422,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p =
       (match p_origin with None -> CErrors.user_err Pp.(str "indeterminate pattern")
       | Some (dir, rule) ->
 	errorstrm (str "indeterminate " ++ pr_dir_side dir
-          ++ str " in " ++ pr_constr_pat rule))
+          ++ str " in " ++ pr_constr_pat env ise rule))
     | LetIn (_, v, _, b) ->
       if b <> mkRel 1 then KpatLet, f, a else KpatFlex, v, a
     | Lambda _ -> KpatLam, f, a
@@ -637,8 +642,8 @@ let assert_done r =
 let assert_done_multires r = 
   match !r with
   | None -> CErrors.anomaly (str"do_once never called.")
-  | Some (n, xs) ->
-      r := Some (n+1,xs);
+  | Some (e, n, xs) ->
+      r := Some (e, n+1,xs);
       try List.nth xs n with Failure _ -> raise NoMatch
 
 type subst = Environ.env -> constr -> constr -> int -> constr
@@ -684,14 +689,15 @@ let mk_tpattern_matcher ?(all_instances=false)
        | _ -> false)
     | _ -> unif_EQ env sigma u.up_f in
 let p2t p = mkApp(p.up_f,p.up_a) in 
-let source () = match upats_origin, upats with
+let source env = match upats_origin, upats with
   | None, [p] -> 
       (if fixed_upat ise p then str"term " else str"partial term ") ++
-      pr_constr_pat (p2t p) ++ spc()
+      pr_constr_pat env ise (p2t p) ++ spc()
   | Some (dir,rule), [p] -> str"The " ++ pr_dir_side dir ++ str" of " ++ 
-      pr_constr_pat rule ++ fnl() ++ ws 4 ++ pr_constr_pat (p2t p) ++ fnl()
+      pr_constr_pat env ise rule ++ fnl() ++ ws 4 ++
+      pr_constr_pat env ise (p2t p) ++ fnl()
   | Some (dir,rule), _ -> str"The " ++ pr_dir_side dir ++ str" of " ++ 
-      pr_constr_pat rule ++ spc()
+      pr_constr_pat env ise rule ++ spc()
   | _, [] | None, _::_::_ ->
       CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin.") in
 let on_instance, instances =
@@ -721,23 +727,23 @@ let rec uniquize = function
       if not all_instances then match_upats_FO upats env sigma0 ise c;
       failed_because_of_TC:=match_upats_HO ~on_instance upats env sigma0 ise c;
       raise NoMatch
-    with FoundUnif sigma_u -> 0,[sigma_u]
+    with FoundUnif sigma_u -> env,0,[sigma_u]
     | (NoMatch|NoProgress) when all_instances && instances () <> [] ->
-      0, uniquize (instances ())
+      env, 0, uniquize (instances ())
     | NoMatch when (not raise_NoMatch) ->
       if !failed_because_of_TC then
-        errorstrm (source ()++strbrk"matches but type classes inference fails")
+        errorstrm (source env++strbrk"matches but type classes inference fails")
       else
-        errorstrm (source () ++ str "does not match any subterm of the goal")
+        errorstrm (source env ++ str "does not match any subterm of the goal")
     | NoProgress when (not raise_NoMatch) ->
         let dir = match upats_origin with Some (d,_) -> d | _ ->
           CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin.") in
-        errorstrm (str"all matches of "++source()++
+        errorstrm (str"all matches of "++source env++
           str"are equal to the " ++ pr_dir_side (inv_dir dir))
     | NoProgress -> raise NoMatch);
   let sigma, _, ({up_f = pf; up_a = pa} as u) =
     if all_instances then assert_done_multires upat_that_matched
-    else List.hd (snd(assert_done upat_that_matched)) in
+    else List.hd (pi3(assert_done upat_that_matched)) in
 (*   pp(lazy(str"sigma@tmatch=" ++ pr_evar_map None sigma)); *)
   if !skip_occ then ((*ignore(k env u.up_t 0);*) c) else
   let match_EQ = match_EQ env sigma u in
@@ -766,18 +772,18 @@ let rec uniquize = function
       mkApp (f', Array.map_left (subst_loop acc) a) in
   subst_loop (env,h) c) : find_P),
 ((fun () ->
-  let sigma, uc, ({up_f = pf; up_a = pa} as u) =
+  let env, (sigma, uc, ({up_f = pf; up_a = pa} as u)) =
     match !upat_that_matched with
-    | Some (_,x) -> List.hd x | None when raise_NoMatch -> raise NoMatch
+    | Some (env,_,x) -> env,List.hd x | None when raise_NoMatch -> raise NoMatch
     | None -> CErrors.anomaly (str"companion function never called.") in
   let p' = mkApp (pf, pa) in
   if max_occ <= !nocc then p', u.up_dir, (sigma, uc, u.up_t)
   else errorstrm (str"Only " ++ int !nocc ++ str" < " ++ int max_occ ++
         str(String.plural !nocc " occurrence") ++ match upats_origin with
-        | None -> str" of" ++ spc() ++ pr_constr_pat p'
+        | None -> str" of" ++ spc() ++ pr_constr_pat env sigma p'
         | Some (dir,rule) -> str" of the " ++ pr_dir_side dir ++ fnl() ++
-            ws 4 ++ pr_constr_pat p' ++ fnl () ++ 
-            str"of " ++ pr_constr_pat rule)) : conclude)
+            ws 4 ++ pr_constr_pat env sigma p' ++ fnl () ++
+            str"of " ++ pr_constr_pat env sigma rule)) : conclude)
 
 type ('ident, 'term) ssrpattern = 
   | T of 'term
@@ -816,11 +822,11 @@ let pr_pattern_aux pr_constr = function
       pr_constr e ++ str " in " ++ pr_constr x ++ str " in " ++ pr_constr t
   | E_As_X_In_T (e,x,t) ->
       pr_constr e ++ str " as " ++ pr_constr x ++ str " in " ++ pr_constr t
-let pp_pattern (sigma, p) =
-  pr_pattern_aux (fun t -> pr_constr_pat (EConstr.Unsafe.to_constr (pi3 (nf_open_term sigma sigma (EConstr.of_constr t))))) p
+let pp_pattern env (sigma, p) =
+  pr_pattern_aux (fun t -> pr_constr_pat env sigma (EConstr.Unsafe.to_constr (pi3 (nf_open_term sigma sigma (EConstr.of_constr t))))) p
 let pr_cpattern = pr_term
 
-let wit_rpatternty = add_genarg "rpatternty" pr_pattern
+let wit_rpatternty = add_genarg "rpatternty" (fun env sigma -> pr_pattern)
 
 let glob_ssrterm gs = function
   | k, (_, Some c), None ->
@@ -1247,8 +1253,10 @@ let fill_occ_term env cl occ sigma0 (sigma, t) =
     if sigma' != sigma0 then raise NoMatch
     else cl, (Evd.merge_universe_context sigma' uc, t')
   with _ ->
-    errorstrm (str "partial term " ++ pr_constr_pat (EConstr.Unsafe.to_constr t)
-            ++ str " does not match any subterm of the goal")
+    errorstrm (str "partial term " ++
+               pr_constr_pat env sigma
+                (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) ++
+               str " does not match any subterm of the goal")
 
 let pf_fill_occ_term gl occ t =
   let sigma0 = project gl and env = pf_env gl and concl = pf_concl gl in
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index ff2c900130..1143bcc813 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -46,7 +46,7 @@ type ('ident, 'term) ssrpattern =
   | E_As_X_In_T of 'term * 'ident * 'term
 
 type pattern = evar_map * (constr, constr) ssrpattern
-val pp_pattern : pattern -> Pp.t
+val pp_pattern : env -> pattern -> Pp.t
 
 (** Extracts the redex and applies to it the substitution part of the pattern.
   @raise Anomaly if called on [In_T] or [In_X_In_T] *)
@@ -222,7 +222,7 @@ val loc_of_cpattern : cpattern -> Loc.t option
 val id_of_pattern : pattern -> Names.Id.t option
 val is_wildcard : cpattern -> bool
 val cpattern_of_id : Names.Id.t -> cpattern
-val pr_constr_pat : constr -> Pp.t
+val pr_constr_pat : env -> evar_map -> constr -> Pp.t
 val pf_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma
 val pf_unsafe_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma
 
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index 13e0bcbd47..73a2b99434 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -37,5 +37,6 @@ END
 VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
   | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
       ident(sc) numnotoption(o) ] ->
-    { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o }
+    { let (sigma, env) = Pfedit.get_current_context () in
+      vernac_numeral_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc) o }
 END
diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg
index 1e06cd8ddb..171e0e213d 100644
--- a/plugins/syntax/g_string.mlg
+++ b/plugins/syntax/g_string.mlg
@@ -21,5 +21,6 @@ open Stdarg
 VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF
   | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":"
       ident(sc) ] ->
-    { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) }
+    { let (sigma, env) = Pfedit.get_current_context () in
+      vernac_string_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc) }
 END
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 0c6d2ac0d1..525056e5f1 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -77,8 +77,7 @@ let locate_int63 () =
     Some (mkRefC q_int63)
   else None
 
-let has_type f ty =
-  let (sigma, env) = Pfedit.get_current_context () in
+let has_type env sigma f ty =
   let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in
   try let _ = Constrintern.interp_constr env sigma c in true
   with Pretype_errors.PretypeError _ -> false
@@ -95,7 +94,7 @@ let type_error_of g ty =
      str " to Decimal.int or (option Decimal.int)." ++ fnl () ++
      str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int could be used (you may need to require BinNums or Decimal or Int63 first).")
 
-let vernac_numeral_notation local ty f g scope opts =
+let vernac_numeral_notation env sigma local ty f g scope opts =
   let int_ty = locate_int () in
   let z_pos_ty = locate_z () in
   let int63_ty = locate_int63 () in
@@ -112,35 +111,35 @@ let vernac_numeral_notation local ty f g scope opts =
   (* Check the type of f *)
   let to_kind =
     match int_ty with
-    | Some (int_ty, cint, _) when has_type f (arrow cint cty) -> Int int_ty, Direct
-    | Some (int_ty, cint, _) when has_type f (arrow cint (opt cty)) -> Int int_ty, Option
-    | Some (int_ty, _, cuint) when has_type f (arrow cuint cty) -> UInt int_ty.uint, Direct
-    | Some (int_ty, _, cuint) when has_type f (arrow cuint (opt cty)) -> UInt int_ty.uint, Option
+    | Some (int_ty, cint, _) when has_type env sigma f (arrow cint cty) -> Int int_ty, Direct
+    | Some (int_ty, cint, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option
+    | Some (int_ty, _, cuint) when has_type env sigma f (arrow cuint cty) -> UInt int_ty.uint, Direct
+    | Some (int_ty, _, cuint) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty.uint, Option
     | _ ->
     match z_pos_ty with
-    | Some (z_pos_ty, cZ) when has_type f (arrow cZ cty) -> Z z_pos_ty, Direct
-    | Some (z_pos_ty, cZ) when has_type f (arrow cZ (opt cty)) -> Z z_pos_ty, Option
+    | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ cty) -> Z z_pos_ty, Direct
+    | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ (opt cty)) -> Z z_pos_ty, Option
     | _ ->
     match int63_ty with
-    | Some cint63 when has_type f (arrow cint63 cty) -> Int63, Direct
-    | Some cint63 when has_type f (arrow cint63 (opt cty)) -> Int63, Option
+    | Some cint63 when has_type env sigma f (arrow cint63 cty) -> Int63, Direct
+    | Some cint63 when has_type env sigma f (arrow cint63 (opt cty)) -> Int63, Option
     | _ -> type_error_to f ty
   in
   (* Check the type of g *)
   let of_kind =
     match int_ty with
-    | Some (int_ty, cint, _) when has_type g (arrow cty cint) -> Int int_ty, Direct
-    | Some (int_ty, cint, _) when has_type g (arrow cty (opt cint)) -> Int int_ty, Option
-    | Some (int_ty, _, cuint) when has_type g (arrow cty cuint) -> UInt int_ty.uint, Direct
-    | Some (int_ty, _, cuint) when has_type g (arrow cty (opt cuint)) -> UInt int_ty.uint, Option
+    | Some (int_ty, cint, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct
+    | Some (int_ty, cint, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option
+    | Some (int_ty, _, cuint) when has_type env sigma g (arrow cty cuint) -> UInt int_ty.uint, Direct
+    | Some (int_ty, _, cuint) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty.uint, Option
     | _ ->
     match z_pos_ty with
-    | Some (z_pos_ty, cZ) when has_type g (arrow cty cZ) -> Z z_pos_ty, Direct
-    | Some (z_pos_ty, cZ) when has_type g (arrow cty (opt cZ)) -> Z z_pos_ty, Option
+    | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty cZ) -> Z z_pos_ty, Direct
+    | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty (opt cZ)) -> Z z_pos_ty, Option
     | _ ->
     match int63_ty with
-    | Some cint63 when has_type g (arrow cty cint63) -> Int63, Direct
-    | Some cint63 when has_type g (arrow cty (opt cint63)) -> Int63, Option
+    | Some cint63 when has_type env sigma g (arrow cty cint63) -> Int63, Direct
+    | Some cint63 when has_type env sigma g (arrow cty (opt cint63)) -> Int63, Option
     | _ -> type_error_of g ty
   in
   let o = { to_kind; to_ty; of_kind; of_ty;
diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
index f96b8321f8..b14ed18497 100644
--- a/plugins/syntax/numeral.mli
+++ b/plugins/syntax/numeral.mli
@@ -14,4 +14,6 @@ open Notation
 
 (** * Numeral notation *)
 
-val vernac_numeral_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit
+val vernac_numeral_notation : Environ.env -> Evd.evar_map -> locality_flag ->
+                              qualid -> qualid -> qualid ->
+                              Notation_term.scope_name -> numnot_option -> unit
diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
index 12ee4c6eda..5fae696d58 100644
--- a/plugins/syntax/string_notation.ml
+++ b/plugins/syntax/string_notation.ml
@@ -32,8 +32,7 @@ let q_option () = qualid_of_ref "core.option.type"
 let q_list () = qualid_of_ref "core.list.type"
 let q_byte () = qualid_of_ref "core.byte.type"
 
-let has_type f ty =
-  let (sigma, env) = Pfedit.get_current_context () in
+let has_type env sigma f ty =
   let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in
   try let _ = Constrintern.interp_constr env sigma c in true
   with Pretype_errors.PretypeError _ -> false
@@ -48,7 +47,7 @@ let type_error_of g ty =
     (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
      str " to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)).")
 
-let vernac_string_notation local ty f g scope =
+let vernac_string_notation env sigma local ty f g scope =
   let app x y = mkAppC (x,[y]) in
   let cref q = mkRefC q in
   let cbyte = cref (q_byte ()) in
@@ -66,18 +65,18 @@ let vernac_string_notation local ty f g scope =
   let constructors = get_constructors tyc in
   (* Check the type of f *)
   let to_kind =
-    if has_type f (arrow clist_byte cty) then ListByte, Direct
-    else if has_type f (arrow clist_byte (opt cty)) then ListByte, Option
-    else if has_type f (arrow cbyte cty) then Byte, Direct
-    else if has_type f (arrow cbyte (opt cty)) then Byte, Option
+    if has_type env sigma f (arrow clist_byte cty) then ListByte, Direct
+    else if has_type env sigma f (arrow clist_byte (opt cty)) then ListByte, Option
+    else if has_type env sigma f (arrow cbyte cty) then Byte, Direct
+    else if has_type env sigma f (arrow cbyte (opt cty)) then Byte, Option
     else type_error_to f ty
   in
   (* Check the type of g *)
   let of_kind =
-    if has_type g (arrow cty clist_byte) then ListByte, Direct
-    else if has_type g (arrow cty (opt clist_byte)) then ListByte, Option
-    else if has_type g (arrow cty cbyte) then Byte, Direct
-    else if has_type g (arrow cty (opt cbyte)) then Byte, Option
+    if has_type env sigma g (arrow cty clist_byte) then ListByte, Direct
+    else if has_type env sigma g (arrow cty (opt clist_byte)) then ListByte, Option
+    else if has_type env sigma g (arrow cty cbyte) then Byte, Direct
+    else if has_type env sigma g (arrow cty (opt cbyte)) then Byte, Option
     else type_error_of g ty
   in
   let o = { to_kind = to_kind;
diff --git a/plugins/syntax/string_notation.mli b/plugins/syntax/string_notation.mli
index 9a0174abf2..e81de603d9 100644
--- a/plugins/syntax/string_notation.mli
+++ b/plugins/syntax/string_notation.mli
@@ -13,4 +13,6 @@ open Vernacexpr
 
 (** * String notation *)
 
-val vernac_string_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> unit
+val vernac_string_notation : Environ.env -> Evd.evar_map -> locality_flag ->
+                             qualid -> qualid -> qualid ->
+                             Notation_term.scope_name -> unit