From bd8b71db33fb9e40575713bc58ae39ccf9f68ab7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 9 Feb 2008 11:31:35 +0000
Subject: Solde de code mort et petites optimisations sur lesquels je suis
 tombé au cours du temps

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10544 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/clenv.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'pretyping/clenv.ml')

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 18a22e5c71..3406d06aa4 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -151,9 +151,6 @@ let mk_clenv_from_n gls n (c,cty) =
 
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
-let mk_clenv_rename_from gls (c,t) = 
-  mk_clenv_from gls (c,rename_bound_var (pf_env gls) [] t)
-
 let mk_clenv_rename_from_n gls n (c,t) = 
   mk_clenv_from_n gls n (c,rename_bound_var (pf_env gls) [] t)
 
-- 
cgit v1.2.3