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.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'proofs/clenv.mli')

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