From 7d122040f6eacbe7e96898f7df86163847e762ed Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 7 Feb 2001 17:44:53 +0000
Subject: code mort

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

diff --git a/tactics/equality.ml b/tactics/equality.ml
index aa031ade69..9b31819279 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1134,14 +1134,6 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
 
  *)
 
-(*
-let comp_carS_squeleton = put_squel mmk "<<x>>(projS1 ? ? (?)@[x])"
-let comp_cdrS_squeleton = put_squel mmk "<<x>>(projS2 ? ? (?)@[x])"
-
-let comp_carT_squeleton = put_squel mmk "<<x>>(projT1 ? ? (?)@[x])"
-let comp_cdrT_squeleton = put_squel mmk "<<x>>(projT2 ? ? (?)@[x])"
-*)
-
 let match_sigma ex ex_pat =
   match matches (get_pat ex_pat) ex with
     | [(1,a);(2,p);(3,car);(4,cdr)] -> (a,p,car,cdr)
-- 
cgit v1.2.3