Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'

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

6 files changed, 19 insertions, 19 deletions

diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 293a81f14..0929d965a 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -202,7 +202,7 @@ Section Zlength_properties.
     case l; auto.
     intros x l'; simpl (length (x :: l')) in |- *.
     rewrite Znat.inj_S.
-    intros; elimtype False; generalize (Zle_0_nat (length l')); omega.
+    intros; exfalso; generalize (Zle_0_nat (length l')); omega.
   Qed.
 
 End Zlength_properties.
diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v
index 512362190..447f6101a 100644
--- a/theories/ZArith/Zgcd_alt.v
+++ b/theories/ZArith/Zgcd_alt.v
@@ -76,7 +76,7 @@ Open Scope Z_scope.
  Proof.
    induction n.
    simpl; intros.
-   elimtype False; generalize (Zabs_pos a); omega.
+   exfalso; generalize (Zabs_pos a); omega.
    destruct a; intros; simpl;
      [ generalize (Zis_gcd_0_abs b); intuition | | ];
    unfold Zmod;
@@ -199,7 +199,7 @@ Open Scope Z_scope.
    0 < a < b -> a < fibonacci (S n) ->
    Zis_gcd a b (Zgcdn n a b).
  Proof.
-   destruct a; [ destruct 1; elimtype False; omega | | destruct 1; discriminate].
+   destruct a; [ destruct 1; exfalso; omega | | destruct 1; discriminate].
    cut (forall k n b,
      k = (S (nat_of_P p) - n)%nat ->
      0 < Zpos p < b -> Zpos p < fibonacci (S n) ->
@@ -254,7 +254,7 @@ Open Scope Z_scope.
  Proof.
    destruct a; intros.
    simpl in H.
-   destruct n; [elimtype False; omega | ].
+   destruct n; [exfalso; omega | ].
    simpl; generalize (Zis_gcd_0_abs b); intuition.
    (*Zpos*)
    generalize (Zgcd_bound_fibonacci (Zpos p)).
@@ -277,8 +277,8 @@ Open Scope Z_scope.
    apply Zgcdn_ok_before_fibonacci; auto.
    apply Zlt_le_trans with (fibonacci (S m)); [ omega | apply fibonacci_incr; auto].
    subst r; simpl.
-   destruct m as [ |m]; [elimtype False; omega| ].
-   destruct n as [ |n]; [elimtype False; omega| ].
+   destruct m as [ |m]; [exfalso; omega| ].
+   destruct n as [ |n]; [exfalso; omega| ].
    simpl; apply Zis_gcd_sym; apply Zis_gcd_0.
    (*Zneg*)
    generalize (Zgcd_bound_fibonacci (Zpos p)).
@@ -303,8 +303,8 @@ Open Scope Z_scope.
    apply Zgcdn_ok_before_fibonacci; auto.
    apply Zlt_le_trans with (fibonacci (S m)); [ omega | apply fibonacci_incr; auto].
    subst r; simpl.
-   destruct m as [ |m]; [elimtype False; omega| ].
-   destruct n as [ |n]; [elimtype False; omega| ].
+   destruct m as [ |m]; [exfalso; omega| ].
+   destruct n as [ |n]; [exfalso; omega| ].
    simpl; apply Zis_gcd_sym; apply Zis_gcd_0.
  Qed.
 
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index 07eca7765..dd46e885d 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -180,7 +180,7 @@ Proof.
   unfold Pminus; rewrite Pminus_mask_diag; auto.
   intros; rewrite Pminus_Lt; auto.
   destruct (Zmax_spec 1 (Zpos p - Zpos q)) as [(H1,H2)|(H1,H2)]; auto.
-  elimtype False; clear H2.
+  exfalso; clear H2.
   assert (H1':=Zlt_trans 0 1 _ Zlt_0_1 H1).
   generalize (Zlt_0_minus_lt _ _ H1').
   unfold Zlt; simpl.
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 3d9853ff0..0fc27e38b 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -66,7 +66,7 @@ Theorem inj_eq_rev : forall n m:nat, Z_of_nat n = Z_of_nat m -> n = m.
 Proof.
   intros x y H.
   destruct (eq_nat_dec x y) as [H'|H']; auto.
-  elimtype False.
+  exfalso.
   exact (inj_neq _ _ H' H).
 Qed.
 
@@ -111,7 +111,7 @@ Theorem inj_le_rev : forall n m:nat, Z_of_nat n <= Z_of_nat m -> (n <= m)%nat.
 Proof.
   intros x y H.
   destruct (le_lt_dec x y) as [H0|H0]; auto.
-  elimtype False.
+  exfalso.
   assert (H1:=inj_lt _ _ H0).
   red in H; red in H1.
   rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto.
@@ -121,7 +121,7 @@ Theorem inj_lt_rev : forall n m:nat, Z_of_nat n < Z_of_nat m -> (n < m)%nat.
 Proof.
   intros x y H.
   destruct (le_lt_dec y x) as [H0|H0]; auto.
-  elimtype False.
+  exfalso.
   assert (H1:=inj_le _ _ H0).
   red in H; red in H1.
   rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto.
@@ -131,7 +131,7 @@ Theorem inj_ge_rev : forall n m:nat, Z_of_nat n >= Z_of_nat m -> (n >= m)%nat.
 Proof.
   intros x y H.
   destruct (le_lt_dec y x) as [H0|H0]; auto.
-  elimtype False.
+  exfalso.
   assert (H1:=inj_gt _ _ H0).
   red in H; red in H1.
   rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto.
@@ -141,7 +141,7 @@ Theorem inj_gt_rev : forall n m:nat, Z_of_nat n > Z_of_nat m -> (n > m)%nat.
 Proof.
   intros x y H.
   destruct (le_lt_dec x y) as [H0|H0]; auto.
-  elimtype False.
+  exfalso.
   assert (H1:=inj_ge _ _ H0).
   red in H; red in H1.
   rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto.
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index dac4a6928..23a2e510f 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -1191,9 +1191,9 @@ Definition prime_dec_aux:
 Proof.
   intros p m.
   case (Z_lt_dec 1 m); intros H1;
-   [ | left; intros; elimtype False; omega ].
+   [ | left; intros; exfalso; omega ].
   pattern m; apply natlike_rec; auto with zarith.
-  left; intros; elimtype False; omega.
+  left; intros; exfalso; omega.
   intros x Hx IH; destruct IH as [F|E].
   destruct (rel_prime_dec x p) as [Y|N].
   left; intros n [HH1 HH2].
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index 40917519e..39aab6331 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -229,9 +229,9 @@ Proof.
   assert (c > 0).
   destruct (Z_le_gt_dec 0 c);trivial.
   destruct (Zle_lt_or_eq _ _ z0);auto with zarith.
-  rewrite <- H3 in H1;simpl in H1; elimtype False;omega.
-  destruct c;try discriminate z0. simpl in H1. elimtype False;omega.
-  assert (H4 := Zpower_lt_monotone a c b H). elimtype False;omega.
+  rewrite <- H3 in H1;simpl in H1; exfalso;omega.
+  destruct c;try discriminate z0. simpl in H1. exfalso;omega.
+  assert (H4 := Zpower_lt_monotone a c b H). exfalso;omega.
 Qed.
 
 Theorem Zpower_nat_Zpower: forall p q, 0 <= q ->