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

6 files changed, 35 insertions, 4 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
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index bb6decd848..5dcbf9b3ef 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -354,14 +354,16 @@ let nf_open_term sigma0 ise c =
   let c' = nf c in let _ = Evd.fold copy_def sigma0 () in
   !s', Evd.evar_universe_context s, EConstr.of_constr c'
 
-let unif_end env sigma0 ise0 pt ok =
+let unif_end ?(solve_TC=true) env sigma0 ise0 pt ok =
   let ise = Evarconv.solve_unif_constraints_with_heuristics env ise0 in
   let tcs = Evd.get_typeclass_evars ise in
   let s, uc, t = nf_open_term sigma0 ise pt in
   let ise1 = create_evar_defs s in
   let ise1 = Evd.set_typeclass_evars ise1 (Evar.Set.filter (fun ev -> Evd.is_undefined ise1 ev) tcs) in
   let ise1 = Evd.set_universe_context ise1 uc in
-  let ise2 = Typeclasses.resolve_typeclasses ~fail:true env ise1 in
+  let ise2 =
+    if solve_TC then Typeclasses.resolve_typeclasses ~fail:true env ise1
+    else ise1 in
   if not (ok ise) then raise NoProgress else
   if ise2 == ise1 then (s, uc, t)
   else
@@ -370,7 +372,7 @@ let unif_end env sigma0 ise0 pt ok =
 
 let unify_HO env sigma0 t1 t2 =
   let sigma = unif_HO env sigma0 t1 t2 in
-  let sigma, uc, _ = unif_end env sigma0 sigma t2 (fun _ -> true) in
+  let sigma, uc, _ = unif_end ~solve_TC:false env sigma0 sigma t2 (fun _ -> true) in
   Evd.set_universe_context sigma uc
 
 let pf_unify_HO gl t1 t2 =
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index f478d48ea3..b3ddb52e85 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -201,7 +201,7 @@ val assert_done : 'a option ref -> 'a
 
 (** Very low level APIs.
     these are calls to evarconv's [the_conv_x] followed by
-    [solve_unif_constraints_with_heuristics] and [resolve_typeclasses].
+    [solve_unif_constraints_with_heuristics].
     In case of failure they raise [NoMatch] *)
 
 val unify_HO : env -> evar_map -> EConstr.constr -> EConstr.constr -> evar_map