Merge PR #8955: [ssr] "case/elim: p" don't resolve TC in "p"

4 files changed, 29 insertions, 0 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index ebe4aac213..be8f3603e4 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -499,6 +499,22 @@ let pf_e_type_of gl t =
   let sigma, ty = Typing.type_of env sigma t in
   re_sig it sigma, ty
 
+let pf_resolve_typeclasses ~where ~fail gl =
+  let sigma, env, it = project gl, pf_env gl, sig_it gl in
+  let filter =
+    let evset = Evarutil.undefined_evars_of_term sigma where in
+    fun k _ -> Evar.Set.mem k evset in
+  let sigma = Typeclasses.resolve_typeclasses ~filter ~fail env sigma in
+  re_sig it sigma
+
+let resolve_typeclasses ~where ~fail env sigma =
+  let filter =
+    let evset = Evarutil.undefined_evars_of_term sigma where in
+    fun k _ -> Evar.Set.mem k evset in
+  let sigma = Typeclasses.resolve_typeclasses ~filter ~fail env sigma in
+  sigma
+
+
 let nf_evar sigma t = 
   EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr t))
 
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 566a933522..cf4e4b354e 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -335,6 +335,14 @@ val refine_with :
            ?beta:bool ->
            ?with_evars:bool ->
            evar_map * EConstr.t -> v82tac
+
+val pf_resolve_typeclasses :
+  where:EConstr.t ->
+  fail:bool -> Goal.goal Evd.sigma -> Goal.goal Evd.sigma
+val resolve_typeclasses :
+  where:EConstr.t ->
+  fail:bool -> Environ.env -> Evd.evar_map -> Evd.evar_map
+
 (*********************** Wrapped Coq  tactics *****************************)
 
 val rewritetac : ssrdir -> EConstr.t -> tactic
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 5067d8af31..d09b81593e 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -353,6 +353,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac
   ppdebug(lazy Pp.(str"elim_pred_ty=" ++ pp_term gl pty));
   let gl = pf_unify_HO gl pred elim_pred in
   let elim = fire_subst gl elim in
+  let gl = pf_resolve_typeclasses ~where:elim ~fail:false gl in
   let gl, _ = pf_e_type_of gl elim in
   (* check that the patterns do not contain non instantiated dependent metas *)
   let () = 
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 036b20bfcd..2a69e3f23a 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -377,6 +377,10 @@ let is_construct_ref sigma c r =
 let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r
 
 let rwcltac cl rdx dir sr gl =
+  let sr =
+    let sigma, r = sr in
+    let sigma = resolve_typeclasses ~where:r ~fail:false (pf_env gl) sigma in
+    sigma, r in
   let n, r_n,_, ucst = pf_abs_evars gl sr in
   let r_n' = pf_abs_cterm gl n r_n in
   let r' = EConstr.Vars.subst_var pattern_id r_n' in