From 89d1b3cf7ba97c2b5e32aaae08e1d913ffc9863f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 15 May 2002 15:17:18 +0000
Subject: Finalement VTactic est gardé pour y plonger les tactiques ML, le
 VTactic utilisé pour les fermetures de ltac s'appelle maintenant VTacticClos

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

(limited to 'tactics')

diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 56f7607235..7f29b4358c 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -109,7 +109,6 @@ let rec tauto_intuit t_reduce t_solver ist =
       $t_solver
    ) >>
 
-(*
 let unfold_not_iff = function
   | None -> interp <:tactic<Unfold not iff>>
   | Some id ->
@@ -119,19 +118,6 @@ let unfold_not_iff = function
 let reduction_not_iff = Tacticals.onAllClauses (fun ido -> unfold_not_iff ido)
 
 let t_reduction_not_iff = 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 = nvar 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