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

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

6 files changed, 99 insertions, 100 deletions

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