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.

---
 proofs/clenv.ml  | 9 ---------
 proofs/clenv.mli | 1 -
 2 files changed, 10 deletions(-)

(limited to 'proofs')

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
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index eb10817069..ca62c985ec 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -49,7 +49,6 @@ val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst
 
 (** {6 linking of clenvs } *)
 
-val connect_clenv : Goal.goal sigma -> clausenv -> clausenv
 val clenv_fchain :
   ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
 
-- 
cgit v1.2.3