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, 16 insertions, 14 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index b7947cddd..0e9bd6e5e 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -1335,20 +1335,21 @@ Definition equal_aux :
  { ~ L.Equal cmp (flatten_e e1) (flatten_e e2) }.
 Proof.
  intros cmp e1 e2; pattern e1, e2 in |- *; apply compare_rec2.
- simple destruct x; simple destruct x'; intuition.
+ simple destruct x; simple destruct x'; intros.
  (* x = x' = End *)
- left; unfold L.Equal in |- *; intuition.
+ left; unfold L.Equal in |- *; split; intros.
+ intuition.
  inversion H2.
  (* x = End x' = More *)
  right; simpl in |- *; auto.
- destruct 1.
+ red; destruct 1.
  destruct (H2 k).
  destruct H5; auto.
  exists e; auto.
  inversion H5.
  (* x = More x' = End *)
  right; simpl in |- *; auto.
- destruct 1.
+ red; destruct 1.
  destruct (H2 k).
  destruct H4; auto.
  exists e; auto.
@@ -1357,7 +1358,7 @@ Proof.
  case (X.compare k k0); intro.
  (* k < k0 *)
  right.
- destruct 1. 
+ red; destruct 1. 
  clear H3 H.
  assert (L.PX.In k (flatten_e (More k0 e3 t0 e4))).
   destruct (H2 k).
@@ -1371,7 +1372,7 @@ Proof.
  intros EQ.
  destruct (@cons t e0) as [c1 (H2,(H3,H4))]; try inversion_clear H0; auto.
  destruct (@cons t0 e4) as [c2 (H5,(H6,H7))]; try inversion_clear H1; auto.
- destruct (H c1 c2); clear H; intuition.
+ destruct (H c1 c2); clear H; intros; auto.
  Measure_e; omega.
  left.
  rewrite H4 in e6; rewrite H7 in e6.
@@ -1382,14 +1383,14 @@ Proof.
  simpl; rewrite <- L.equal_cons; auto.
  apply (sorted_flatten_e H0).
  apply (sorted_flatten_e H1).
- swap f.
+ contradict n.
  rewrite H4; rewrite H7; auto.
  right.
- destruct 1.
+ red; destruct 1.
  rewrite (H4 k) in H2; try discriminate; simpl; auto.
  (* k > k0 *)
  right.
- destruct 1. 
+ red; destruct 1. 
  clear H3 H.
  assert (L.PX.In k0 (flatten_e (More k e t e0))).
   destruct (H2 k0).
@@ -1422,13 +1423,14 @@ Proof.
  inversion_clear 2.
  simpl in a; rewrite <- app_nil_end in a.
  simpl in a0; rewrite <- app_nil_end in a0.
- destruct (@equal_aux cmp x x0); intuition.
+ decompose [and] a; decompose [and] a0.
+ destruct (@equal_aux cmp x x0); auto.
  left.
- rewrite H4 in e; rewrite H5 in e.
+ rewrite H2 in e; rewrite H5 in e.
  rewrite Equal_elements; auto.
  right.
- swap n.
- rewrite H4; rewrite H5.
+ contradict n.
+ rewrite H2; rewrite H5.
  rewrite <- Equal_elements; auto.
 Qed.
 
@@ -1586,7 +1588,7 @@ inversion H1; auto.
 intros.
 inversion_clear H1.
 assert (~X.eq x k).
- swap H5.
+ contradict H5.
  destruct H3.
  apply InA_eqA with (x,x0); eauto.
 apply (H2 x).