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

3 files changed, 6 insertions, 6 deletions

diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index c7632d185..a0111a082 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 f02baca2c..aee2cf8f7 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 e0f3fdf4b..c2c7767d5 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.