small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is

more general.



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

1 files changed, 17 insertions, 17 deletions

diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 0afdf5d00..dca6e5498 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -221,10 +221,10 @@ Proof.
  destruct a as (x',e').
  simpl; case (X.eq_dec x x'); inversion_clear Hm; auto.
  constructor; auto.
- swap H.
+ contradict H.
  apply InA_eqk with (x,e); auto.
  constructor; auto.
- swap H; apply add_3' with x e; auto.
+ contradict H; apply add_3' with x e; auto.
 Qed.
 
 (* Not part of the exported specifications, used later for [combine]. *)
@@ -272,8 +272,8 @@ Proof.
 
  inversion_clear Hm.
  subst.
- swap H0.
- destruct H2 as (e,H2); unfold PX.MapsTo in H2.
+ contradict H0.
+ destruct H0 as (e,H2); unfold PX.MapsTo in H2.
  apply InA_eqk with (y,e); auto.
  compute; apply X.eq_trans with x; auto.
   
@@ -323,7 +323,7 @@ Proof.
  destruct a as (x',e').
  simpl; case (X.eq_dec x x'); auto.
  constructor; auto.
- swap H; apply remove_3' with x; auto.
+ contradict H; apply remove_3' with x; auto.
 Qed.  
 
 (** * [elements] *)
@@ -533,12 +533,12 @@ Proof.
  destruct a as (x',e').
  inversion_clear Hm.
  constructor; auto.
- swap H.
+ contradict H.
  (* il faut un map_1 avec eqk au lieu de eqke *)
  clear IHm H0. 
  induction m; simpl in *; auto.
- inversion H1.
- destruct a; inversion H1; auto.
+ inversion H.
+ destruct a; inversion H; auto.
 Qed.      
  
 (** Specification of [mapi] *)
@@ -593,11 +593,11 @@ Proof.
  destruct a as (x',e').
  inversion_clear Hm; auto.
  constructor; auto.
- swap H.
+ contradict H.
  clear IHm H0.
  induction m; simpl in *; auto.
- inversion_clear H1.
- destruct a; inversion_clear H1; auto.
+ inversion_clear H.
+ destruct a; inversion_clear H; auto.
 Qed.
 
 End Elt2. 
@@ -765,13 +765,13 @@ Proof.
  inversion_clear H1.
  destruct a; destruct o; simpl; auto.
  constructor; auto.
- swap H.
+ contradict H.
  clear IHl1.
  induction l1.
- inversion H1.
+ inversion H.
  inversion_clear H0.
  destruct a; destruct o; simpl in *; auto.
- inversion_clear  H1; auto.
+ inversion_clear H; auto.
 Qed.
 
 Definition at_least_one_then_f (o:option elt)(o':option elt') := 
@@ -807,7 +807,7 @@ Proof.
  rewrite H2.
  unfold f'; simpl.
  destruct (f oo oo'); simpl. 
- destruct (X.eq_dec x k); try absurd_hyp n; auto.
+ destruct (X.eq_dec x k); try contradict n; auto.
  destruct (IHm0 H1) as (_,H4); apply H4; auto.
  case_eq (find x m0); intros; auto.
  elim H0.
@@ -817,7 +817,7 @@ Proof.
  (* k < x *)
  unfold f'; simpl.
  destruct (f oo oo'); simpl.
- destruct (X.eq_dec x k); [ absurd_hyp n; auto | auto].
+ destruct (X.eq_dec x k); [ contradict n; auto | auto].
  destruct (IHm0 H1) as (H3,_); apply H3; auto.
  destruct (IHm0 H1) as (H3,_); apply H3; auto.
 
@@ -831,7 +831,7 @@ Proof.
  (* k < x *)
  unfold f'; simpl.
  destruct (f oo oo'); simpl.
- destruct (X.eq_dec x k); [ absurd_hyp n; auto | auto].
+ destruct (X.eq_dec x k); [ contradict n; auto | auto].
  destruct (IHm0 H1) as (_,H4); apply H4; auto.
  destruct (IHm0 H1) as (_,H4); apply H4; auto.
 Qed.