diff options
| author | coqbot-app[bot] | 2020-12-18 15:52:16 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-18 15:52:16 +0000 |
| commit | 82d0a578b91f4de87deebc658b0e085646ca63d4 (patch) | |
| tree | 0319a8f8f880d8d4585c04062560067fda039f3b /tactics/equality.ml | |
| parent | 8013852eb0957141181110a904aeff7b37a8219d (diff) | |
| parent | 7a8761b0ca9c503592c14ee98402e530cde28846 (diff) | |
Merge PR #13628: Cache meta instances in Clenv
Reviewed-by: mattam82
Reviewed-by: gares
Ack-by: SkySkimmer
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index fcdd23a9c1..633b9da053 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -154,7 +154,8 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = let c1 = args.(arglen - 2) in let c2 = args.(arglen - 1) in let try_occ (evd', c') = - Clenv.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'} + let clenv = Clenv.update_clenv_evd eqclause evd' in + Clenv.clenv_pose_dependent_evars ~with_evars:true clenv in let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in let occs = |