From e9892fadb99ae56bf759c6013c7cccc07b31adab Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 4 Oct 2000 15:55:35 +0000
Subject: Code mort

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@651 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/equality.ml | 11 +----------
 1 file changed, 1 insertion(+), 10 deletions(-)

diff --git a/tactics/equality.ml b/tactics/equality.ml
index dcf09b5f1..e0a8c8541 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1175,16 +1175,7 @@ let subst_tuple_term env sigma dep_pair b =
   let abst_B =
     List.fold_right
       (fun (e,t) body -> lambda_create env (t,subst_term e body)) e_list b in
-  let app_B = applist(abst_B,proj_list) in
-  (* inutile ?? les projs sont appliquées à (mkRel 1) ?? *)
-(*
-  let { proj1 = proj1_sp; proj2 = proj2_sp; elim = sig_elim_sp } =
-    find_sigma_data (get_sort_of env sigma typ) in
-  strong (fun _ _ -> 
-	    compose (whd_betaiota env sigma)
-	      (whd_const [proj1_sp;proj2_sp;sig_elim_sp] env sigma)) 
-    env sigma *)
-  (* whd_betaiota *) app_B
+  let app_B = applist(abst_B,proj_list) in app_B
     
 (* |- (P e2)
      BY RevSubstInConcl (eq T e1 e2)
-- 
cgit v1.2.3