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

2 files changed, 8 insertions, 8 deletions

diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index ae5e2d444..d6eea61c8 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 8747a4c44..e8c292992 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.