Nettoyage

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2737 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 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))