From 17210c01d0d0b9cbc6c1870b421a7eff2adc1d99 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 13 Nov 2018 09:52:18 +0100
Subject: ssr: rewrite: do resolve TC once and forall at the very end

---
 plugins/ssr/ssrequality.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'plugins')

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
-- 
cgit v1.2.3