Inlining the only use of Clenv.connect_clenv.

1 files changed, 0 insertions, 9 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index ae790d9b82..bc6e75c38d 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -345,15 +345,6 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
 
 (******************************************************************)
 
-let connect_clenv gls clenv =
-  let evd = evars_reset_evd ~with_conv_pbs:true gls.sigma clenv.evd in
-  { clenv with
-    evd = evd ;
-    env = Goal.V82.env evd (sig_it gls) }
-
-(* let connect_clenv_key = Profile.declare_profile "connect_clenv";; *)
-(* let connect_clenv = Profile.profile2 connect_clenv_key connect_clenv *)
-
 (* [clenv_fchain mv clenv clenv']
  *
  * Resolves the value of "mv" (which must be undefined) in clenv to be