From 5ccadc40d54090df5e6b61b4ecbb6083d01e5a88 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 18 Nov 2015 00:56:29 +0100
Subject: Inlining the only use of Clenv.connect_clenv.

---
 tactics/class_tactics.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 8ee3ec9281..4f0ffa024e 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -158,9 +158,9 @@ let e_give_exact flags poly (c,clenv) gl =
   let c, gl =
     if poly then
       let clenv', subst = Clenv.refresh_undefined_univs clenv in
-      let clenv' = connect_clenv gl clenv' in
+      let evd = evars_reset_evd ~with_conv_pbs:true gl.sigma clenv'.evd in
       let c = Vars.subst_univs_level_constr subst c in
-	c, {gl with sigma = clenv'.evd}
+	c, {gl with sigma = evd}
     else c, gl
   in
   let t1 = pf_unsafe_type_of gl c in
-- 
cgit v1.2.3