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 ---
 pretyping/clenv.mli | 3 ---
 2 files changed, 6 deletions(-)

(limited to 'pretyping')

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)
 
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index e6cd960b20..1697bb3c2b 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -53,9 +53,6 @@ val clenv_meta_type : clausenv -> metavariable -> types
 val mk_clenv_from : evar_info sigma -> constr * types -> clausenv
 val mk_clenv_from_n :
   evar_info sigma -> int option -> constr * types -> clausenv
-val mk_clenv_rename_from : evar_info sigma -> constr * types -> clausenv
-val mk_clenv_rename_from_n :
-  evar_info sigma -> int option -> constr * types -> clausenv
 val mk_clenv_type_of : evar_info sigma -> constr -> clausenv
 
 (***************************************************************)
-- 
cgit v1.2.3