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
---
 proofs/tacmach.ml  | 8 --------
 proofs/tacmach.mli | 1 -
 2 files changed, 9 deletions(-)

(limited to 'proofs')

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 68cd194799..7fd7aabe40 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -217,14 +217,6 @@ let mutual_fix f n others gl =
 let mutual_cofix f others gl = 
   with_check (refiner (Prim (Cofix (f,others)))) gl
     
-let rename_bound_var_goal gls =
-  let { evar_hyps = sign; evar_concl = cl } = sig_it gls in 
-  let ids = ids_of_named_context (named_context_of_val sign) in
-  convert_concl_no_check 
-    (rename_bound_var (Global.env()) ids cl) DEFAULTcast gls 
-
-
-
 (* Versions with consistency checks *)
 
 let introduction id    = with_check (introduction_no_check id) 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index ed95ef285a..6b6305a177 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -136,7 +136,6 @@ val rename_hyp_no_check       : (identifier*identifier) list -> tactic
 val mutual_fix      :
   identifier -> int -> (identifier * int * constr) list -> tactic
 val mutual_cofix    : identifier -> (identifier * constr) list -> tactic
-val rename_bound_var_goal : tactic
 
 (*s The most primitive tactics with consistency and type checking *)
 
-- 
cgit v1.2.3