diff options
| author | Enrico Tassi | 2018-11-13 09:52:18 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-11-14 10:49:59 +0100 |
| commit | 17210c01d0d0b9cbc6c1870b421a7eff2adc1d99 (patch) | |
| tree | 6b68436f31fd2bf298a9ffcd44ea863991c6a450 /plugins | |
| parent | 68197ed162d0dd5e3a1b9bf490a81b6e840a8408 (diff) | |
ssr: rewrite: do resolve TC once and forall at the very end
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 4 |
1 files changed, 4 insertions, 0 deletions
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 |