Merge PR #6173: [printing] Deprecate all printing functions accessing the global proof.

8 files changed, 46 insertions, 43 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index c1d7e6278..83b454769 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -240,7 +240,7 @@ let interp_refine ist gl rc =
   in
   let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in
 (*   ppdebug(lazy(str"sigma@interp_refine=" ++ pr_evar_map None sigma)); *)
-  ppdebug(lazy(str"c@interp_refine=" ++ Printer.pr_econstr c));
+  ppdebug(lazy(str"c@interp_refine=" ++ Printer.pr_econstr_env (pf_env gl) sigma c));
   (sigma, (sigma, c))
 
 
@@ -539,7 +539,7 @@ module Intset = Evar.Set
 
 let pf_abs_evars_pirrel gl (sigma, c0) =
   pp(lazy(str"==PF_ABS_EVARS_PIRREL=="));
-  pp(lazy(str"c0= " ++ Printer.pr_constr c0));
+  pp(lazy(str"c0= " ++ Printer.pr_constr_env (pf_env gl) sigma c0));
   let sigma0 = project gl in
   let c0 = nf_evar sigma0 (nf_evar sigma c0) in
   let nenv = env_size (pf_env gl) in
@@ -563,7 +563,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
   | _ -> Constr.fold put evlist c in
   let evlist = put [] c0 in
   if evlist = [] then 0, c0 else
-  let pr_constr t = Printer.pr_econstr (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in
+  let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in
   pp(lazy(str"evlist=" ++ pr_list (fun () -> str";")
     (fun (k,_) -> str(Evd.string_of_existential k)) evlist));
   let evplist = 
@@ -959,7 +959,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl =
               loop (meta_declare m (EConstr.Unsafe.to_constr ty) sigma) bo ((EConstr.mkMeta m)::args) (n-1)
           | _ -> assert false
       in loop sigma t [] n in
-    pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr t));
+    pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t));
     Tacmach.refine_no_check t gl
 
 let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
@@ -973,7 +973,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
     compose_lam (let xs,y = List.chop (n-1) l in y @ xs) 
       (mkApp (compose_lam l c, Array.of_list (mkRel 1 :: mkRels n)))
   in
-  pp(lazy(str"after: " ++ Printer.pr_constr oc));
+  pp(lazy(str"after: " ++ Printer.pr_constr_env (pf_env gl) (project gl) oc));
   try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl
   with e when CErrors.noncritical e -> raise dependent_apply_error
 
@@ -1202,7 +1202,7 @@ let genclrtac cl cs clr =
 let gentac ist gen gl =
 (*   ppdebug(lazy(str"sigma@gentac=" ++ pr_evar_map None (project gl))); *)
   let conv, _, cl, c, clr, ucst,gl = pf_interp_gen_aux ist gl false gen in
-  ppdebug(lazy(str"c@gentac=" ++ pr_econstr c));
+  ppdebug(lazy(str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c));
   let gl = pf_merge_uc ucst gl in
   if conv
   then tclTHEN (Proofview.V82.of_tactic (convert_concl cl)) (cleartac clr) gl
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 26b5c5767..4e0b44a44 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -46,7 +46,7 @@ let analyze_eliminator elimty env sigma =
     if not (EConstr.eq_constr sigma t t') then loop ctx t' else
       errorstrm Pp.(str"The eliminator has the wrong shape."++spc()++
       str"A (applied) bound variable was expected as the conclusion of "++
-      str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr elimty) in
+      str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr_env env' sigma elimty) in
   let ctx, pred_id, elim_is_dep, n_pred_args,concl = loop [] elimty in
   let n_elim_args = Context.Rel.nhyps ctx in
   let is_rec_elim = 
@@ -126,7 +126,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) ?ist deps what ?elim eqid elim_intr
     ppdebug(lazy Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern 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 c));
+    ppdebug(lazy Pp.(str"     got: " ++ pr_constr_env env sigma0 c));
     c, EConstr.of_constr cl, ucst in
   let mkTpat gl t = (* takes a term, refreshes it and makes a T pattern *)
     let n, t, _, ucst = pf_abs_evars orig_gl (project gl, fire_subst gl t) in 
@@ -239,8 +239,8 @@ let ssrelim ?(ind=ref None) ?(is_case=false) ?ist deps what ?elim eqid elim_intr
       | Some (c, _, _,gl) -> true, gl
       | None ->
         errorstrm Pp.(str"Unable to apply the eliminator to the term"++
-          spc()++pr_econstr c++spc()++str"or to unify it's type with"++
-          pr_econstr inf_arg_ty) in
+          spc()++pr_econstr_env env (project gl) c++spc()++str"or to unify it's type with"++
+          pr_econstr_env env (project gl) inf_arg_ty) in
   ppdebug(lazy Pp.(str"c_is_head_p= " ++ bool c_is_head_p));
   let gl, predty = pfe_type_of gl pred in
   (* Patterns for the inductive types indexes to be bound in pred are computed
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index e82f222b9..274c7110c 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -77,7 +77,7 @@ let interp_congrarg_at ist gl n rf ty m =
     if i + n > m then None else
     try
       let rt = mkRApp congrn (args1 @  mkRApp rf (mkRHoles i) :: args2) in
-      ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr rt));
+      ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) rt));
       Some (interp_refine ist gl rt)
     with _ -> loop (i + 1) in
   loop 0
@@ -86,7 +86,7 @@ let pattern_id = mk_internal_id "pattern value"
 
 let congrtac ((n, t), ty) ist gl =
   ppdebug(lazy (Pp.str"===congr==="));
-  ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr (Tacmach.pf_concl gl)));
+  ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl)));
   let sigma, _ as it = interp_term ist gl t in
   let gl = pf_merge_uc_of sigma gl in
   let _, f, _, _ucst = pf_abs_evars gl it in
@@ -109,7 +109,7 @@ let congrtac ((n, t), ty) ist gl =
 
 let newssrcongrtac arg ist gl =
   ppdebug(lazy Pp.(str"===newcongr==="));
-  ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr (pf_concl gl)));
+  ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl)));
   (* utils *)
   let fs gl t = Reductionops.nf_evar (project gl) t in
   let tclMATCH_GOAL (c, gl_c) proj t_ok t_fail gl =
@@ -247,7 +247,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 c)),
+        ++ pr_constr_pat (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")
@@ -267,13 +267,13 @@ let unfoldintac occ rdx t (kt,_) gl =
             | Proj _ when same_proj sigma0 c t -> body env t c
             | Const f -> aux (body env c c)
             | App (f, a) -> aux (EConstr.mkApp (body env f f, a))
-            | _ -> errorstrm Pp.(str "The term "++pr_constr orig_c++
-                str" contains no " ++ pr_econstr t ++ str" even after unfolding")
+            | _ -> errorstrm Pp.(str "The term "++ pr_constr_env env sigma orig_c++
+                str" contains no " ++ pr_econstr_env env sigma t ++ str" even after unfolding")
           in EConstr.Unsafe.to_constr @@ aux (EConstr.of_constr c)
       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 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 (EConstr.Unsafe.to_constr t))),
     fake_pmatcher_end in
   let concl = 
     let concl0 = EConstr.Unsafe.to_constr concl0 in
@@ -352,7 +352,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
   (* We check the proof is well typed *)
   let sigma, proof_ty =
     try Typing.type_of env sigma proof with _ -> raise PRtype_error in
-  ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr proof_ty));
+  ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr_env env sigma proof_ty));
   try refine_with 
     ~first_goes_last:(not !ssroldreworder) ~with_evars:false (sigma, proof) gl
   with _ -> 
@@ -374,8 +374,8 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
           if open_evs <> [] then Some name else None)
           (List.combine (Array.to_list args) names)
     | _ -> anomaly "rewrite rule not an application" in
-    errorstrm Pp.(Himsg.explain_refiner_error (Logic.UnresolvedBindings miss)++
-      (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr hd_ty))
+    errorstrm Pp.(Himsg.explain_refiner_error env sigma (Logic.UnresolvedBindings miss)++
+      (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr_env env sigma hd_ty))
 ;;
 
 let is_construct_ref sigma c r =
@@ -391,12 +391,12 @@ let rwcltac cl rdx dir sr gl =
   let gl = pf_unsafe_merge_uc ucst gl in
   let rdxt = Retyping.get_type_of (pf_env gl) (fst sr) rdx in
 (*         ppdebug(lazy(str"sigma@rwcltac=" ++ pr_evar_map None (fst sr))); *)
-        ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr (snd sr)));
+        ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env (pf_env gl) (project gl) (snd sr)));
   let cvtac, rwtac, gl =
     if EConstr.Vars.closed0 (project gl) r' then 
       let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.build_coq_eq () in
       let sigma, c_ty = Typing.type_of env sigma c in
-        ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr c_ty));
+        ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty));
       match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with
       | AtomicType(e, a) when is_ind_ref sigma e c_eq ->
           let new_rdx = if dir = L2R then a.(2) else a.(1) in
@@ -411,7 +411,7 @@ let rwcltac cl rdx dir sr gl =
       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))
-                    ++ str " to " ++ pr_econstr r2) in
+                    ++ str " to " ++ pr_econstr_env (pf_env gl) (project gl) r2) in
       let cl' = EConstr.mkNamedProd rule_id (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in
       let cl'' = EConstr.mkNamedProd pattern_id rdxt cl' in
       let itacs = [introid pattern_id; introid rule_id] in
@@ -605,7 +605,7 @@ let ssrinstancesofrule ist dir arg gl =
       sigma, pats @ [pat] in
     let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in
     mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma0 None ~upats_origin rpats in
-  let print env p c _ = Feedback.msg_info Pp.(hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in
+  let print env p c _ = Feedback.msg_info Pp.(hov 1 (str"instance:" ++ spc() ++ pr_constr_env env r_sigma p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr_env env r_sigma c)); c in
   Feedback.msg_info Pp.(str"BEGIN INSTANCES");
   try
     while true do
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 29e96ec59..a707226cd 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -72,13 +72,14 @@ let examine_abstract id gl =
   let gl, tid = pfe_type_of gl id in
   let abstract, gl = pf_mkSsrConst "abstract" gl in
   let sigma = project gl in
+  let env = pf_env gl in
   if not (EConstr.isApp sigma tid) || not (EConstr.eq_constr sigma (fst(EConstr.destApp sigma tid)) abstract) then
-    errorstrm(strbrk"not an abstract constant: "++pr_econstr id);
+    errorstrm(strbrk"not an abstract constant: "++ pr_econstr_env env sigma id);
   let _, args_id = EConstr.destApp sigma tid in
   if Array.length args_id <> 3 then
-    errorstrm(strbrk"not a proper abstract constant: "++pr_econstr id);
+    errorstrm(strbrk"not a proper abstract constant: "++ pr_econstr_env env sigma id);
   if not (is_Evar_or_CastedMeta sigma args_id.(2)) then
-    errorstrm(strbrk"abstract constant "++pr_econstr id++str" already used");
+    errorstrm(strbrk"abstract constant "++ pr_econstr_env env sigma id++str" already used");
   tid, args_id
 
 let pf_find_abstract_proof check_lock gl abstract_n = 
@@ -94,7 +95,7 @@ let pf_find_abstract_proof check_lock gl abstract_n =
     | _ -> l) (project gl) [] in
   match l with
   | [e] -> e
-  | _ -> errorstrm(strbrk"abstract constant "++pr_constr abstract_n++
+  | _ -> errorstrm(strbrk"abstract constant "++ pr_constr_env (pf_env gl) (project gl) abstract_n ++
            strbrk" not found in the evar map exactly once. "++
            strbrk"Did you tamper with it?")
 
@@ -205,7 +206,7 @@ let havetac ist
      let assert_is_conv gl =
        try Proofview.V82.of_tactic (convert_concl (EConstr.it_mkProd_or_LetIn concl ctx)) gl
        with _ -> errorstrm (str "Given proof term is not of type " ++
-         pr_econstr (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) concl)) in
+         pr_econstr_env (pf_env gl) (project gl) (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) concl)) in
      gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c
    | FwdHave, false, false ->
      let skols = List.flatten (List.map (function
@@ -271,7 +272,7 @@ let ssrabstract ist gens (*last*) gl =
     let gl, proof =
       let pf_unify_HO gl a b =
         try pf_unify_HO gl a b
-        with _ -> errorstrm(strbrk"The abstract variable "++pr_econstr id++
+        with _ -> errorstrm(strbrk"The abstract variable "++ pr_econstr_env env (project gl) id++
           strbrk" cannot abstract this goal.  Did you generalize it?") in
       let find_hole p t =
         match EConstr.kind (project gl) t with
@@ -290,7 +291,7 @@ let ssrabstract ist gens (*last*) gl =
         | App(hd, [|left; right|]) when Term.Constr.equal hd prod ->
             find_hole (mkApp (proj1,[|left;right;p|])) left
 *)
-        | _ -> errorstrm(strbrk"abstract constant "++pr_econstr abstract_n++
+        | _ -> errorstrm(strbrk"abstract constant "++ pr_econstr_env env (project gl) abstract_n++
                strbrk" has an unexpected shape. Did you tamper with it?")
       in
         find_hole
@@ -361,14 +362,14 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
       | Sort _, [] -> EConstr.Vars.subst_vars s ct
       | LetIn(Name id as n,b,ty,c), _::g -> EConstr.mkLetIn (n,b,ty,var2rel c g (id::s))
       | Prod(Name id as n,ty,c), _::g -> EConstr.mkProd (n,ty,var2rel c g (id::s))
-      | _ -> CErrors.anomaly(str"SSR: wlog: var2rel: " ++ pr_econstr c) in
+      | _ -> CErrors.anomaly(str"SSR: wlog: var2rel: " ++ pr_econstr_env env sigma c) in
     let c = var2rel c gens [] in
     let rec pired c = function
       | [] -> c
       | t::ts as args -> match EConstr.kind sigma c with
          | Prod(_,_,c) -> pired (EConstr.Vars.subst1 t c) ts
          | LetIn(id,b,ty,c) -> EConstr.mkLetIn (id,b,ty,pired c args)
-         | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr c) in
+         | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr_env env sigma c) in
     c, args, pired c args, pf_merge_uc uc gl in
   let tacipat pats = introstac ~ist pats in
   let tacigens = 
@@ -396,8 +397,8 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
       | Some id ->
         if pats = [] then Tacticals.tclIDTAC else
         let args = Array.of_list args in
-        ppdebug(lazy(str"specialized="++pr_econstr EConstr.(mkApp (mkVar id,args))));
-        ppdebug(lazy(str"specialized_ty="++pr_econstr ct));
+        ppdebug(lazy(str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args))));
+        ppdebug(lazy(str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct));
         Tacticals.tclTHENS (basecuttac "ssr_have" ct)
           [Proofview.V82.of_tactic (Tactics.apply EConstr.(mkApp (mkVar id,args))); Tacticals.tclIDTAC] in
       "ssr_have",
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 023778fdb..6c325cce4 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -272,7 +272,7 @@ let (introstac : ?ist:Tacinterp.interp_sign -> ssripats -> Tacmach.tactic),
 let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr gl =
   (* Utils of local interest only *)
   let iD s ?t gl = let t = match t with None -> pf_concl gl | Some x -> x in
-                   ppdebug(lazy Pp.(str s ++ pr_econstr t)); Tacticals.tclIDTAC gl in
+                   ppdebug(lazy Pp.(str s ++ pr_econstr_env (pf_env gl) (project gl) t)); Tacticals.tclIDTAC gl in
   let protectC, gl = pf_mkSsrConst "protect_term" gl in
   let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in
   let eq = EConstr.of_constr eq in
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 7b591fead..46403aef3 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -1131,7 +1131,7 @@ let pr_fwd_guarded prval prval' = function
 | (fk, h), (_, (_, Some c)) ->
   pr_gen_fwd prval pr_constr_expr prl_constr_expr fk (format_constr_expr h c)
 | (fk, h), (_, (c, None)) ->
-  pr_gen_fwd prval' pr_glob_constr prl_glob_constr fk (format_glob_constr h c)
+  pr_gen_fwd prval' pr_glob_constr_env prl_glob_constr fk (format_glob_constr h c)
 
 let pr_unguarded prc prlc = prlc
 
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index e865ef706..4b2fab6d1 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -24,7 +24,7 @@ let pp_concat hd ?(sep=str", ") = function [] -> hd | x :: xs ->
   hd ++ List.fold_left (fun acc x -> acc ++ sep ++ x) x xs
 
 let pp_term gl t =
-  let t = Reductionops.nf_evar (project gl) t in pr_econstr t
+  let t = Reductionops.nf_evar (project gl) t in pr_econstr_env (pf_env gl) (project gl) t
 
 (* FIXME *)
 (* terms are pre constr, the kind is parsing/printing flag to distinguish
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 36dce37ae..cd614fee9 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -343,7 +343,7 @@ let coerce_search_pattern_to_sort hpat =
   let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in
   let warn () =
     Feedback.msg_warning (str "Listing only lemmas with conclusion matching " ++ 
-      pr_constr_pattern hpat') in
+      pr_constr_pattern_env env sigma hpat') in
   if EConstr.isSort sigma ht then begin warn (); true, hpat' end else
   let filter_head, coe_path =
     try 
@@ -359,7 +359,7 @@ let coerce_search_pattern_to_sort hpat =
       let n_imps = Option.get (Classops.hide_coercion coe_ref) in
       mkPApp (Pattern.PRef coe_ref) n_imps [|hp|]
     with _ ->
-    errorstrm (str "need explicit coercion " ++ pr_constr coe ++ spc ()
+    errorstrm (str "need explicit coercion " ++ pr_constr_env env sigma coe ++ spc ()
             ++ str "to interpret head search pattern as type") in
   filter_head, List.fold_left coerce hpat' coe_path
 
@@ -468,10 +468,12 @@ let pr_raw_ssrhintref prc _ _ = let open CAst in function
     prc c ++ str "|" ++ int (List.length args)
   | c -> prc c
 
-let pr_rawhintref c = match DAst.get c with
+let pr_rawhintref c =
+  let _, env = Pfedit.get_current_context () in
+  match DAst.get c with
   | GApp (f, args) when isRHoles args ->
-    pr_glob_constr f ++ str "|" ++ int (List.length args)
-  | _ -> pr_glob_constr c
+    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