From 161b7b47f7f87c33f1fa6269248d5f8b6b4926d9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Dec 2020 21:09:11 +0100
Subject: Make the clenv type private and provide a creation function.

---
 tactics/equality.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tactics/equality.ml')

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