aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrcommon.ml12
-rw-r--r--plugins/ssr/ssrelim.ml8
-rw-r--r--plugins/ssr/ssrequality.ml28
-rw-r--r--plugins/ssr/ssrfwd.ml23
-rw-r--r--plugins/ssr/ssripats.ml2
-rw-r--r--plugins/ssr/ssrparser.ml42
-rw-r--r--plugins/ssr/ssrprinters.ml2
-rw-r--r--plugins/ssr/ssrvernac.ml412
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-11 21:30:15 +0000