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

7 files changed, 23 insertions, 23 deletions

diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
index 03c6114422..89c37c0f9b 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
@@ -931,7 +931,7 @@ Section DoubleDivGt.
    case (spec_to_Z (w_head0 bh)); auto with zarith.
    assert ([|w_head0 bh|] < Zpos w_digits).
     destruct (Z_lt_ge_dec [|w_head0 bh|]  (Zpos w_digits));trivial.
-    elimtype False.
+    exfalso.
     assert (2 ^ [|w_head0 bh|] * [|bh|] >= wB);auto with zarith.
     apply Zle_ge; replace wB with (wB * 1);try ring.
     Spec_w_to_Z bh;apply Zmult_le_compat;zarith.
@@ -1071,7 +1071,7 @@ Section DoubleDivGt.
              (WW ah al) bl).
    rewrite spec_w_0W;unfold ww_to_Z;trivial.
    apply spec_ww_div_gt_aux;trivial. rewrite spec_w_0 in Hcmp;trivial.
-   rewrite spec_w_0 in Hcmp;elimtype False;omega.
+   rewrite spec_w_0 in Hcmp;exfalso;omega.
   Qed.
 
   Lemma spec_ww_mod_gt_aux_eq : forall ah al bh bl,
@@ -1243,7 +1243,7 @@ Section DoubleDivGt.
    rewrite  (@spec_double_modn1 w w_digits w_zdigits w_0 w_WW); trivial.
    apply Zlt_gt;match goal with | |- ?x mod ?y < ?y =>
     destruct (Z_mod_lt x y);zarith end.
-   rewrite spec_w_0 in Hbl;Spec_w_to_Z bl;elimtype False;omega.
+   rewrite spec_w_0 in Hbl;Spec_w_to_Z bl;exfalso;omega.
    rewrite spec_w_0 in Hbh;assert (H:= spec_ww_mod_gt_aux _ _ _ Hgt Hbh).
    assert (H2 : 0 < [[WW bh bl]]).
    simpl;Spec_w_to_Z bl. apply Zlt_le_trans with ([|bh|]*wB);zarith.
@@ -1265,7 +1265,7 @@ Section DoubleDivGt.
    rewrite  (@spec_double_modn1 w w_digits w_zdigits w_0 w_WW); trivial.
    apply Zlt_gt;match goal with | |- ?x mod ?y < ?y =>
    destruct (Z_mod_lt x y);zarith end.
-   rewrite spec_w_0 in Hml;Spec_w_to_Z ml;elimtype False;omega.
+   rewrite spec_w_0 in Hml;Spec_w_to_Z ml;exfalso;omega.
    rewrite spec_w_0 in Hmh. assert ([[WW bh bl]] > [[WW mh ml]]).
    rewrite H;simpl; apply Zlt_gt;match goal with | |- ?x mod ?y < ?y =>
    destruct (Z_mod_lt x y);zarith end.
@@ -1300,8 +1300,8 @@ Section DoubleDivGt.
    rewrite Z_div_mult;zarith.
    assert (2^1 <= 2^n). change (2^1) with 2;zarith.
    assert (H7 := @Zpower_le_monotone_inv 2 1 n);zarith.
-   rewrite spec_w_0 in Hmh;Spec_w_to_Z mh;elimtype False;zarith.
-   rewrite spec_w_0 in Hbh;Spec_w_to_Z bh;elimtype False;zarith.
+   rewrite spec_w_0 in Hmh;Spec_w_to_Z mh;exfalso;zarith.
+   rewrite spec_w_0 in Hbh;Spec_w_to_Z bh;exfalso;zarith.
   Qed.
 
   Lemma spec_ww_gcd_gt_aux :
@@ -1473,7 +1473,7 @@ Section DoubleDiv.
    simpl;rewrite H;simpl;destruct (w_compare w_1 yl).
    rewrite spec_ww_1;rewrite <- Hcmpy;apply Zis_gcd_mod;zarith.
    rewrite <- (Zmod_unique ([|xh|]*wB+[|xl|]) 1 ([|xh|]*wB+[|xl|]) 0);zarith.
-   rewrite H in Hle; elimtype False;zarith.
+   rewrite H in Hle; exfalso;zarith.
    assert ([|yl|] = 0). Spec_w_to_Z yl;zarith.
    rewrite H0;simpl;apply Zis_gcd_0;trivial.
   Qed.
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index ee4ea3c726..74c893594e 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -162,9 +162,9 @@ destruct (Zlt_trichotomy n 0) as [H1 | [H1 | H1]];
 [| rewrite H2 in H; rewrite Zmul_0_r in H; false_hyp H Zlt_irrefl |]);
 try (left; now split); try (right; now split).
 assert (H3 : n * m > 0) by now apply Zmul_neg_neg.
-elimtype False; now apply (Zlt_asymm (n * m) 0).
+exfalso; now apply (Zlt_asymm (n * m) 0).
 assert (H3 : n * m > 0) by now apply Zmul_pos_pos.
-elimtype False; now apply (Zlt_asymm (n * m) 0).
+exfalso; now apply (Zlt_asymm (n * m) 0).
 now apply Zmul_neg_pos. now apply Zmul_pos_neg.
 Qed.
 
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index ae5e2d4447..d6eea61c8c 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -219,10 +219,10 @@ intros n m; split.
 intro H; destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]];
 destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]];
 try (now right); try (now left).
-elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZmul_neg_neg |].
-elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZmul_neg_pos |].
-elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZmul_pos_neg |].
-elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZmul_pos_pos |].
+exfalso; now apply (NZlt_neq 0 (n * m)); [apply NZmul_neg_neg |].
+exfalso; now apply (NZlt_neq (n * m) 0); [apply NZmul_neg_pos |].
+exfalso; now apply (NZlt_neq (n * m) 0); [apply NZmul_pos_neg |].
+exfalso; now apply (NZlt_neq 0 (n * m)); [apply NZmul_pos_pos |].
 intros [H | H]. now rewrite H, NZmul_0_l. now rewrite H, NZmul_0_r.
 Qed.
 
@@ -260,9 +260,9 @@ destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]];
 [| rewrite H2 in H; rewrite NZmul_0_r in H; false_hyp H NZlt_irrefl |]);
 try (left; now split); try (right; now split).
 assert (H3 : n * m < 0) by now apply NZmul_neg_pos.
-elimtype False; now apply (NZlt_asymm (n * m) 0).
+exfalso; now apply (NZlt_asymm (n * m) 0).
 assert (H3 : n * m < 0) by now apply NZmul_pos_neg.
-elimtype False; now apply (NZlt_asymm (n * m) 0).
+exfalso; now apply (NZlt_asymm (n * m) 0).
 now apply NZmul_pos_pos. now apply NZmul_neg_neg.
 Qed.
 
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 8747a4c44a..e8c2929928 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -184,7 +184,7 @@ split; intros H H1 H2.
 apply NZlt_le_incl; le_elim H2; [now apply H | now rewrite H2 in H1].
 assert (n <= p) as H3. apply H. assumption. now apply NZlt_le_incl.
 le_elim H3. assumption. rewrite <- H3 in H2.
-elimtype False; now apply (NZlt_asymm n m).
+exfalso; now apply (NZlt_asymm n m).
 Qed.
 
 Theorem NZle_trans : forall n m p : NZ, n <= m -> m <= p -> n <= p.
@@ -209,7 +209,7 @@ Qed.
 Theorem NZle_antisymm : forall n m : NZ, n <= m -> m <= n -> n == m.
 Proof.
 intros n m H1 H2; now (le_elim H1; le_elim H2);
-[elimtype False; apply (NZlt_asymm n m) | | |].
+[exfalso; apply (NZlt_asymm n m) | | |].
 Qed.
 
 Theorem NZlt_1_l : forall n m : NZ, 0 < n -> n < m -> 1 < m.
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index c7632d1859..a0111a082c 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -187,16 +187,16 @@ Qed.
 Theorem succ_pred : forall n : N, n ~= 0 -> S (P n) == n.
 Proof.
 cases n.
-intro H; elimtype False; now apply H.
+intro H; exfalso; now apply H.
 intros; now rewrite pred_succ.
 Qed.
 
 Theorem pred_inj : forall n m : N, n ~= 0 -> m ~= 0 -> P n == P m -> n == m.
 Proof.
 intros n m; cases n.
-intros H; elimtype False; now apply H.
+intros H; exfalso; now apply H.
 intros n _; cases m.
-intros H; elimtype False; now apply H.
+intros H; exfalso; now apply H.
 intros m H2 H3. do 2 rewrite pred_succ in H3. now rewrite H3.
 Qed.
 
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index f02baca2cf..aee2cf8f74 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -455,7 +455,7 @@ Qed.
 Theorem lt_pred_l : forall n : N, n ~= 0 -> P n < n.
 Proof.
 cases n.
-intro H; elimtype False; now apply H.
+intro H; exfalso; now apply H.
 intros; rewrite pred_succ;  apply lt_succ_diag_r.
 Qed.
 
diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v
index e0f3fdf4bb..c2c7767d5a 100644
--- a/theories/Numbers/Natural/Binary/NBinDefs.v
+++ b/theories/Numbers/Natural/Binary/NBinDefs.v
@@ -160,11 +160,11 @@ Theorem NZlt_succ_r : forall n m : NZ, n < (NZsucc m) <-> n <= m.
 Proof.
 intros n m; unfold Nlt, Nle; destruct n as [| p]; destruct m as [| q]; simpl;
 split; intro H; try reflexivity; try discriminate.
-destruct p; simpl; intros; discriminate. elimtype False; now apply H.
+destruct p; simpl; intros; discriminate. exfalso; now apply H.
 apply -> Pcompare_p_Sq in H. destruct H as [H | H].
 now rewrite H. now rewrite H, Pcompare_refl.
 apply <- Pcompare_p_Sq. case_eq ((p ?= q)%positive Eq); intro H1.
-right; now apply Pcompare_Eq_eq. now left. elimtype False; now apply H.
+right; now apply Pcompare_Eq_eq. now left. exfalso; now apply H.
 Qed.
 
 Theorem NZmin_l : forall n m : N, n <= m -> NZmin n m = n.