From 49db22be8b253900362f210ebd800ba1d326e589 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Fri, 28 Mar 2003 13:30:24 +0000
Subject: Fixed Relative names not,iff in Camlp4 quotation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3799 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/newtauto.ml4 |  9 ++-------
 tactics/tauto.ml4    | 21 ++++++++++++---------
 2 files changed, 14 insertions(+), 16 deletions(-)

diff --git a/tactics/newtauto.ml4 b/tactics/newtauto.ml4
index f378bbe803..04ecc36fa2 100644
--- a/tactics/newtauto.ml4
+++ b/tactics/newtauto.ml4
@@ -56,10 +56,7 @@ let isrec ind=
   let (mib,mip) = Global.lookup_inductive ind in
   Inductiveops.mis_is_recursive (ind,mib,mip)
 
-let simplif=interp
- <:tactic<Repeat (Match Context With 
-		 |[|- ?]->Progress Unfold not iff 
-		 |[H:?|- ?]->Progress Unfold not iff in H)>>
+let simplif=Tauto.reduction_not_iff
 
 let rule_axiom=assumption
 		      
@@ -207,9 +204,7 @@ let q_elim tac=
   let vtac=Tacexpr.TacArg (valueIn (VTactic tac)) in	
   interp <:tactic<
   Match Context With 
-   [x:?1|-(? ?1 ?)]->
-      Exists x;$vtac  
-  |[x:?1;H:?1->?|-?]->
+    [x:?1;H:?1->?|-?]->
       Generalize (H x);Clear H;$vtac>>
 
 let rec lfo n=
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 2a0a01f43d..36ee7e18a6 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -52,12 +52,12 @@ let not_dep_intros ist =
   Repeat
     Match Context With
 | [|- ?1 -> ?2 ] -> Intro
-| [|- (iff ? ?)] -> Unfold iff
-| [|- (not ?)] -> Unfold not
-| [ H:(iff ? ?)|- ?] -> Unfold iff in H
-| [ H:(not ?)|-?] -> Unfold not in H
-| [ H:(iff ? ?)->?|- ?] -> Unfold iff in H
-| [ H:(not ?)->?|-?] -> Unfold not in H >>
+| [|- (Coq.Init.Logic.iff ? ?)] -> Unfold Coq.Init.Logic.iff
+| [|- (Coq.Init.Logic.not ?)] -> Unfold Coq.Init.Logic.not
+| [ H:(Coq.Init.Logic.iff ? ?)|- ?] -> Unfold Coq.Init.Logic.iff in H
+| [ H:(Coq.Init.Logic.not ?)|-?] -> Unfold Coq.Init.Logic.not in H
+| [ H:(Coq.Init.Logic.iff ? ?)->?|- ?] -> Unfold Coq.Init.Logic.iff in H
+| [ H:(Coq.Init.Logic.not ?)->?|-?] -> Unfold Coq.Init.Logic.not in H >>
 				      
 let axioms ist =
   let t_is_unit = tacticIn is_unit
@@ -136,9 +136,12 @@ let rec tauto_intuit t_reduce t_solver ist =
    ) >>
     
 let reduction_not_iff=interp
- <:tactic<Repeat (Match Context With 
-		 |[|- ?]->Progress Unfold not iff 
-		 |[H:?|- ?]->Progress Unfold not iff in H)>>
+ <:tactic<Repeat 
+	(Match Context With 
+	|[|- ?]->
+	   Progress Unfold Coq.Init.Logic.not Coq.Init.Logic.iff 
+	|[H:?|- ?]->
+	   Progress Unfold Coq.Init.Logic.not Coq.Init.Logic.iff in H)>>
 
 
 let t_reduction_not_iff = Tacexpr.TacArg (valueIn (VTactic reduction_not_iff))
-- 
cgit v1.2.3