From bbc73182d6d5006ba348794c664fac742e78a8f2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 30 May 2002 14:16:49 +0000
Subject: Nettoyage

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

diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 2e266a29d7..07175f73b7 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -119,20 +119,6 @@ let reduction_not_iff =
 
 let t_reduction_not_iff = Tacexpr.TacArg (valueIn (VTactic reduction_not_iff))
 
-(*
-let reduction_not_iff ist =
-  match ist.goalopt with 
-    | None -> anomaly "reduction_not_iff"
-    | Some gl ->
-	List.fold_right
-	(fun id tac -> 
-	  let id = (dummy_loc,id) in <:tactic<Unfold not iff in $id; $tac>>)
-	(Tacmach.pf_ids_of_hyps gl)
-	<:tactic<Unfold not iff>>
-
-let t_reduction_not_iff = tacticIn reduction_not_iff
-*)
-
 let intuition_gen tac =
   interp (tacticIn (tauto_intuit t_reduction_not_iff tac))
 
-- 
cgit v1.2.3