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

31 files changed, 113 insertions, 96 deletions

diff --git a/CHANGES b/CHANGES
index 72ef742f4..19b51b4e3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -39,6 +39,8 @@ Tactics
   is interpreted as using the collection of its constructors.
 - Tactic names "case" and "elim" now support clauses "as" and "in" and become
   then synonymous of "destruct" and "induction" respectively.
+- An new name "exfalso" for the use of 'ex-falso quodlibet' principle.
+  This tactic is simply a shortcut for "elimtype False".
 
 Tactic Language
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 6dbdaedd4..01816a396 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1115,6 +1115,15 @@ the following way:
 \item  {\tt H: A $\vd$ $\neg$B} \ becomes \ {\tt H: B $\vd$ $\neg$A}
 \end{itemize}
 
+\subsection{\tt exfalso}
+\label{exfalso}
+\tacindex{exfalso}
+
+This tactic implements the ``ex falso quodlibet'' logical principle:
+an elimination of {\tt False} is performed on the current goal, and the
+user is then required to prove that {\tt False} is indeed provable in
+the current context. This tactic is a macro for {\tt elimtype False}.
+
 \section{Conversion tactics
 \index{Conversion tactics}
 \label{Conversion-tactics}}
diff --git a/plugins/field/LegacyField_Theory.v b/plugins/field/LegacyField_Theory.v
index 378efa035..cc8b043fc 100644
--- a/plugins/field/LegacyField_Theory.v
+++ b/plugins/field/LegacyField_Theory.v
@@ -602,7 +602,7 @@ simpl in |- *; fold AoppT in |- *; case (eqExprA (EAopp e0) (EAinv a));
 unfold monom_remove in |- *; case (eqExprA (EAinv e0) (EAinv a)); intros.
 case (eqExprA e0 a); intros.
 rewrite e2; simpl in |- *; fold AinvT in |- *; rewrite AinvT_r; auto.
-inversion e1; simpl in |- *; elimtype False; auto.
+inversion e1; simpl in |- *; exfalso; auto.
 simpl in |- *; trivial.
 unfold monom_remove in |- *; case (eqExprA (EAvar n) (EAinv a)); intros;
  [ inversion e0 | simpl in |- *; trivial ].
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index a97f43d08..c82abfc85 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -583,7 +583,7 @@ Module IntProperties (I:Int).
  Proof.
  intros.
  destruct (lt_eq_lt_dec n 0) as [[Hn|Hn]|Hn]; auto;
-  destruct (lt_eq_lt_dec m 0) as [[Hm|Hm]|Hm]; auto; elimtype False.
+  destruct (lt_eq_lt_dec m 0) as [[Hm|Hm]|Hm]; auto; exfalso.
 
  rewrite lt_0_neg' in Hn.
  rewrite lt_0_neg' in Hm.
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 10924769e..5565c048c 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -1909,7 +1909,7 @@ Module OrdProperties (M:S).
   rewrite add_mapsto_iff; unfold O.eqke; simpl.
   intuition.
   destruct (E.eq_dec x t0); auto.
-  elimtype False.
+  exfalso.
   assert (In t0 m).
    exists e0; auto.
   generalize (H t0 H1).
@@ -1939,7 +1939,7 @@ Module OrdProperties (M:S).
   rewrite add_mapsto_iff; unfold O.eqke; simpl.
   intuition.
   destruct (E.eq_dec x t0); auto.
-  elimtype False.
+  exfalso.
   assert (In t0 m).
    exists e0; auto.
   generalize (H t0 H1).
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index c4b8f2a8d..afac5af8c 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -108,7 +108,7 @@ Lemma height_0 : forall l, avl l -> height l = 0 ->
  l = Leaf _.
 Proof.
  destruct 1; intuition; simpl in *.
- avl_nns; simpl in *; elimtype False; omega_max.
+ avl_nns; simpl in *; exfalso; omega_max.
 Qed.
 
 
diff --git a/theories/FSets/FSetFullAVL.v b/theories/FSets/FSetFullAVL.v
index d8a31ba5f..bc2b7b64e 100644
--- a/theories/FSets/FSetFullAVL.v
+++ b/theories/FSets/FSetFullAVL.v
@@ -98,7 +98,7 @@ Ltac avl_nns :=
 Lemma height_0 : forall s, avl s -> height s = 0 -> s = Leaf.
 Proof.
  destruct 1; intuition; simpl in *.
- avl_nns; simpl in *; elimtype False; omega_max.
+ avl_nns; simpl in *; exfalso; omega_max.
 Qed.
 
 (** * Results about [avl] *)
@@ -755,7 +755,7 @@ Proof.
  intros s1 s2 B1 B2.
  generalize (ocaml_compare_Cmp s1 s2)(compare_Cmp s1 s2).
  unfold Cmp.
- destruct ocaml_compare; destruct compare; auto; intros; elimtype False.
+ destruct ocaml_compare; destruct compare; auto; intros; exfalso.
  elim (lt_not_eq B1 B2 H0); auto.
  elim (lt_not_eq B2 B1 H0); auto.
   apply eq_sym; auto.
diff --git a/theories/FSets/OrderedType.v b/theories/FSets/OrderedType.v
index 4e5d39faf..f17eb43a9 100644
--- a/theories/FSets/OrderedType.v
+++ b/theories/FSets/OrderedType.v
@@ -149,7 +149,7 @@ Ltac abstraction := match goal with
  | H : eq ?x ?x |- _ => clear H; abstraction
  | H : ~lt ?x ?x |- _ => clear H; abstraction
  | |- eq ?x ?x => exact (eq_refl x)
- | |- lt ?x ?x => elimtype False; abstraction
+ | |- lt ?x ?x => exfalso; abstraction
  | |- ~ _ => intro; abstraction
  | H1: ~lt ?x ?y, H2: ~eq ?x ?y |- _ =>
      generalize (le_neq H1 H2); clear H1 H2; intro; abstraction
@@ -240,7 +240,7 @@ Ltac order :=
  propagate_lt;
  eauto.
 
-Ltac false_order := elimtype False; order.
+Ltac false_order := exfalso; order.
 
   Lemma gt_not_eq : forall x y, lt y x -> ~ eq x y.
   Proof.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 0d36d40e3..6ccf8a022 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -14,6 +14,12 @@ Require Import Specif.
 
 (** * Useful tactics *)
 
+(** Ex falso quodlibet : a tactic for proving False instead of the current goal.
+    This is just a nicer name for tactics such as [elimtype False]
+    and other [cut False]. *)
+
+Ltac exfalso := elimtype False.
+
 (** A tactic for proof by contradiction. With contradict H,
     -   H:~A |-  B    gives       |-  A
     -   H:~A |- ~B    gives  H: B |-  A
@@ -31,7 +37,7 @@ Ltac contradict H :=
   let negneg H := save negpos H
   in
   let pospos H :=
-    let A := type of H in (elimtype False; revert H; try fold (~A))
+    let A := type of H in (exfalso; revert H; try fold (~A))
   in
   let posneg H := save pospos H
   in
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index b1f2668e6..a35682767 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -503,7 +503,7 @@ Qed.
 Lemma N0_less_2 : forall a, Nless N0 a = false -> a = N0.
 Proof.
   induction a as [|p]; intro H. trivial.
-  elimtype False. induction p as [|p IHp|]; discriminate || simpl; auto using IHp.
+  exfalso. induction p as [|p IHp|]; discriminate || simpl; auto using IHp.
 Qed.
 
 Lemma Nless_trans :
@@ -692,7 +692,7 @@ Definition Bnth (n:nat)(bv:Bvector n)(p:nat) : p<n -> bool.
 Proof.
  induction 1.
  intros.
- elimtype False; inversion H.
+ exfalso; inversion H.
  intros.
  destruct p.
  exact a.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
index 03c611442..89c37c0f9 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 ee4ea3c72..74c893594 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 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.
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.
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index ca65f3bbe..0c77a1325 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -374,7 +374,7 @@ Ltac simplify_one_dep_elim_term c :=
     | @eq ?A ?t ?u -> ?P => apply (noConfusion (I:=A) P)
     | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H)
     | ?t = ?u -> _ => let hyp := fresh in
-      intros hyp ; elimtype False ; discriminate
+      intros hyp ; exfalso ; discriminate
     | ?x = ?y -> _ => let hyp := fresh in
       intros hyp ; (try (clear hyp ; (* If non dependent, don't clear it! *) fail 1)) ;
         case hyp ; clear hyp
@@ -447,7 +447,7 @@ Ltac try_intros m :=
 (** To solve a goal by inversion on a particular target. *)
 
 Ltac solve_empty target :=
-  do_nat target intro ; elimtype False ; destruct_last ; simplify_dep_elim.
+  do_nat target intro ; exfalso ; destruct_last ; simplify_dep_elim.
 
 Ltac simplify_method tac := repeat (tac || simplify_one_dep_elim) ; reverse_local.
 
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 0fe8bb176..2b6af10ec 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1283,8 +1283,8 @@ Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
 Proof.
   intros z x y H H0.
   case (Rtotal_order x y); intros Eq0; auto; elim Eq0; clear Eq0; intros Eq0.
-  rewrite Eq0 in H0; elimtype False; apply (Rlt_irrefl (z * y)); auto.
-  generalize (Rmult_lt_compat_l z y x H Eq0); intro; elimtype False;
+  rewrite Eq0 in H0; exfalso; apply (Rlt_irrefl (z * y)); auto.
+  generalize (Rmult_lt_compat_l z y x H Eq0); intro; exfalso;
     generalize (Rlt_trans (z * x) (z * y) (z * x) H0 H1);
       intro; apply (Rlt_irrefl (z * x)); auto.
 Qed.
@@ -1619,11 +1619,11 @@ Hint Resolve pos_INR: real.
 Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat.
 Proof.
   double induction n m; intros.
-  simpl in |- *; elimtype False; apply (Rlt_irrefl 0); auto.
+  simpl in |- *; exfalso; apply (Rlt_irrefl 0); auto.
   auto with arith.
   generalize (pos_INR (S n0)); intro; cut (INR 0 = 0);
     [ intro H2; rewrite H2 in H0; idtac | simpl in |- *; trivial ].
-  generalize (Rle_lt_trans 0 (INR (S n0)) 0 H1 H0); intro; elimtype False;
+  generalize (Rle_lt_trans 0 (INR (S n0)) 0 H1 H0); intro; exfalso;
     apply (Rlt_irrefl 0); auto.
   do 2 rewrite S_INR in H1; cut (INR n1 < INR n0).
   intro H2; generalize (H0 n0 H2); intro; auto with arith.
@@ -1665,7 +1665,7 @@ Proof.
   intros n m H; case (le_or_lt n m); intros H1.
   case (le_lt_or_eq _ _ H1); intros H2.
   apply Rlt_dichotomy_converse; auto with real.
-  elimtype False; auto.
+  exfalso; auto.
   apply sym_not_eq; apply Rlt_dichotomy_converse; auto with real.
 Qed.
 Hint Resolve not_INR: real.
@@ -1675,10 +1675,10 @@ Proof.
   intros; case (le_or_lt n m); intros H1.
   case (le_lt_or_eq _ _ H1); intros H2; auto.
   cut (n <> m).
-  intro H3; generalize (not_INR n m H3); intro H4; elimtype False; auto.
+  intro H3; generalize (not_INR n m H3); intro H4; exfalso; auto.
   omega.
   symmetry  in |- *; cut (m <> n).
-  intro H3; generalize (not_INR m n H3); intro H4; elimtype False; auto.
+  intro H3; generalize (not_INR m n H3); intro H4; exfalso; auto.
   omega.
 Qed.
 Hint Resolve INR_eq: real.
@@ -1884,7 +1884,7 @@ Lemma IZR_lt : forall n m:Z, (n < m)%Z -> IZR n < IZR m.
 Proof.
   intros m n H; cut (m <= n)%Z.
   intro H0; elim (IZR_le m n H0); intro; auto.
-  generalize (eq_IZR m n H1); intro; elimtype False; omega.
+  generalize (eq_IZR m n H1); intro; exfalso; omega.
   omega.
 Qed.
 
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index f5570286d..7588020c5 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -294,7 +294,7 @@ Definition Rabs r : R :=
 Lemma Rabs_R0 : Rabs 0 = 0.
 Proof.
   unfold Rabs in |- *; case (Rcase_abs 0); auto; intro.
-  generalize (Rlt_irrefl 0); intro; elimtype False; auto.
+  generalize (Rlt_irrefl 0); intro; exfalso; auto.
 Qed.
 
 Lemma Rabs_R1 : Rabs 1 = 1.
@@ -356,7 +356,7 @@ Definition RRle_abs := Rle_abs.
 Lemma Rabs_pos_eq : forall x:R, 0 <= x -> Rabs x = x.
 Proof.
   intros; unfold Rabs in |- *; case (Rcase_abs x); intro;
-    [ generalize (Rgt_not_le 0 x r); intro; elimtype False; auto | trivial ].
+    [ generalize (Rgt_not_le 0 x r); intro; exfalso; auto | trivial ].
 Qed.
 
 (*********)
@@ -370,7 +370,7 @@ Lemma Rabs_pos_lt : forall x:R, x <> 0 -> 0 < Rabs x.
 Proof.
   intros; generalize (Rabs_pos x); intro; unfold Rle in H0; elim H0; intro;
     auto.
-  elimtype False; clear H0; elim H; clear H; generalize H1; unfold Rabs in |- *;
+  exfalso; clear H0; elim H; clear H; generalize H1; unfold Rabs in |- *;
     case (Rcase_abs x); intros; auto.
   clear r H1; generalize (Rplus_eq_compat_l x 0 (- x) H0);
     rewrite (let (H1, H2) := Rplus_ne x in H1); rewrite (Rplus_opp_r x);
@@ -383,14 +383,14 @@ Proof.
   intros; unfold Rabs in |- *; case (Rcase_abs (x - y));
     case (Rcase_abs (y - x)); intros.
   generalize (Rminus_lt y x r); generalize (Rminus_lt x y r0); intros;
-    generalize (Rlt_asym x y H); intro; elimtype False;
+    generalize (Rlt_asym x y H); intro; exfalso;
       auto.
   rewrite (Ropp_minus_distr x y); trivial.
   rewrite (Ropp_minus_distr y x); trivial.
   unfold Rge in r, r0; elim r; elim r0; intros; clear r r0.
   generalize (Ropp_lt_gt_0_contravar (x - y) H); rewrite (Ropp_minus_distr x y);
     intro; unfold Rgt in H0; generalize (Rlt_asym 0 (y - x) H0);
-      intro; elimtype False; auto.
+      intro; exfalso; auto.
   rewrite (Rminus_diag_uniq x y H); trivial.
   rewrite (Rminus_diag_uniq y x H0); trivial.
   rewrite (Rminus_diag_uniq y x H0); trivial.
@@ -403,46 +403,46 @@ Proof.
     case (Rcase_abs y); intros; auto.
   generalize (Rmult_lt_gt_compat_neg_l y x 0 r r0); intro;
     rewrite (Rmult_0_r y) in H; generalize (Rlt_asym (x * y) 0 r1);
-      intro; unfold Rgt in H; elimtype False; rewrite (Rmult_comm y x) in H;
+      intro; unfold Rgt in H; exfalso; rewrite (Rmult_comm y x) in H;
         auto.
   rewrite (Ropp_mult_distr_l_reverse x y); trivial.
   rewrite (Rmult_comm x (- y)); rewrite (Ropp_mult_distr_l_reverse y x);
     rewrite (Rmult_comm x y); trivial.
   unfold Rge in r, r0; elim r; elim r0; clear r r0; intros; unfold Rgt in H, H0.
   generalize (Rmult_lt_compat_l x 0 y H H0); intro; rewrite (Rmult_0_r x) in H1;
-    generalize (Rlt_asym (x * y) 0 r1); intro; elimtype False;
+    generalize (Rlt_asym (x * y) 0 r1); intro; exfalso;
       auto.
   rewrite H in r1; rewrite (Rmult_0_l y) in r1; generalize (Rlt_irrefl 0);
-    intro; elimtype False; auto.
+    intro; exfalso; auto.
   rewrite H0 in r1; rewrite (Rmult_0_r x) in r1; generalize (Rlt_irrefl 0);
-    intro; elimtype False; auto.
+    intro; exfalso; auto.
   rewrite H0 in r1; rewrite (Rmult_0_r x) in r1; generalize (Rlt_irrefl 0);
-    intro; elimtype False; auto.
+    intro; exfalso; auto.
   rewrite (Rmult_opp_opp x y); trivial.
   unfold Rge in r, r1; elim r; elim r1; clear r r1; intros; unfold Rgt in H0, H.
   generalize (Rmult_lt_compat_l y x 0 H0 r0); intro;
     rewrite (Rmult_0_r y) in H1; rewrite (Rmult_comm y x) in H1;
-      generalize (Rlt_asym (x * y) 0 H1); intro; elimtype False;
+      generalize (Rlt_asym (x * y) 0 H1); intro; exfalso;
         auto.
   generalize (Rlt_dichotomy_converse x 0 (or_introl (x > 0) r0));
     generalize (Rlt_dichotomy_converse y 0 (or_intror (y < 0) H0));
       intros; generalize (Rmult_integral x y H); intro;
-        elim H3; intro; elimtype False; auto.
+        elim H3; intro; exfalso; auto.
   rewrite H0 in H; rewrite (Rmult_0_r x) in H; unfold Rgt in H;
-    generalize (Rlt_irrefl 0); intro; elimtype False;
+    generalize (Rlt_irrefl 0); intro; exfalso;
       auto.
   rewrite H0; rewrite (Rmult_0_r x); rewrite (Rmult_0_r (- x)); trivial.
   unfold Rge in r0, r1; elim r0; elim r1; clear r0 r1; intros;
     unfold Rgt in H0, H.
   generalize (Rmult_lt_compat_l x y 0 H0 r); intro; rewrite (Rmult_0_r x) in H1;
-    generalize (Rlt_asym (x * y) 0 H1); intro; elimtype False;
+    generalize (Rlt_asym (x * y) 0 H1); intro; exfalso;
       auto.
   generalize (Rlt_dichotomy_converse y 0 (or_introl (y > 0) r));
     generalize (Rlt_dichotomy_converse 0 x (or_introl (0 > x) H0));
       intros; generalize (Rmult_integral x y H); intro;
-        elim H3; intro; elimtype False; auto.
+        elim H3; intro; exfalso; auto.
   rewrite H0 in H; rewrite (Rmult_0_l y) in H; unfold Rgt in H;
-    generalize (Rlt_irrefl 0); intro; elimtype False;
+    generalize (Rlt_irrefl 0); intro; exfalso;
       auto.
   rewrite H0; rewrite (Rmult_0_l y); rewrite (Rmult_0_l (- y)); trivial.
 Qed.
@@ -454,14 +454,14 @@ Proof.
     intros.
   apply Ropp_inv_permute; auto.
   generalize (Rinv_lt_0_compat r r1); intro; unfold Rge in r0; elim r0; intros.
-  unfold Rgt in H1; generalize (Rlt_asym 0 (/ r) H1); intro; elimtype False;
+  unfold Rgt in H1; generalize (Rlt_asym 0 (/ r) H1); intro; exfalso;
     auto.
   generalize (Rlt_dichotomy_converse (/ r) 0 (or_introl (/ r > 0) H0)); intro;
-    elimtype False; auto.
+    exfalso; auto.
   unfold Rge in r1; elim r1; clear r1; intro.
   unfold Rgt in H0; generalize (Rlt_asym 0 (/ r) (Rinv_0_lt_compat r H0));
-    intro; elimtype False; auto.
-  elimtype False; auto.
+    intro; exfalso; auto.
+  exfalso; auto.
 Qed.
 
 Lemma Rabs_Ropp : forall x:R, Rabs (- x) = Rabs x.
@@ -478,7 +478,7 @@ Proof.
   generalize (Ropp_le_ge_contravar 0 (-1) H1).
   rewrite Ropp_involutive; rewrite Ropp_0.
   intro; generalize (Rgt_not_le 1 0 Rlt_0_1); intro; generalize (Rge_le 0 1 H2);
-    intro; elimtype False; auto.
+    intro; exfalso; auto.
   ring.
 Qed.
 
@@ -505,7 +505,7 @@ Proof.
       clear v w; rewrite (Rplus_opp_l a) in H0; apply (Rlt_trans (- a) 0 a H0 H).
   right; rewrite H; apply Ropp_0.
 (**)
-  elimtype False; generalize (Rplus_ge_compat_l a b 0 r); intro;
+  exfalso; generalize (Rplus_ge_compat_l a b 0 r); intro;
     elim (Rplus_ne a); intros v w; rewrite v in H; clear v w;
       generalize (Rge_trans (a + b) a 0 H r0); intro; clear H;
         unfold Rge in H0; elim H0; intro; clear H0.
@@ -513,7 +513,7 @@ Proof.
   absurd (a + b = 0); auto.
   apply (Rlt_dichotomy_converse (a + b) 0); left; assumption.
 (**)
-  elimtype False; generalize (Rplus_lt_compat_l a b 0 r); intro;
+  exfalso; generalize (Rplus_lt_compat_l a b 0 r); intro;
     elim (Rplus_ne a); intros v w; rewrite v in H; clear v w;
       generalize (Rlt_trans (a + b) a 0 H r0); intro; clear H;
         unfold Rge in r1; elim r1; clear r1; intro.
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v
index 3309f7d50..55982aa54 100644
--- a/theories/Reals/Rderiv.v
+++ b/theories/Reals/Rderiv.v
@@ -168,7 +168,7 @@ Proof.
       rewrite eps2 in H10; assumption.
   unfold Rabs in |- *; case (Rcase_abs 2); auto.
   intro; cut (0 < 2).
-  intro; generalize (Rlt_asym 0 2 H7); intro; elimtype False; auto.
+  intro; generalize (Rlt_asym 0 2 H7); intro; exfalso; auto.
   fourier.
   apply Rabs_no_R0.
   discrR.
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index a57bb1638..11be9772e 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -113,7 +113,7 @@ Hint Resolve pow_lt: real.
 Lemma Rlt_pow_R1 : forall (x:R) (n:nat), 1 < x -> (0 < n)%nat -> 1 < x ^ n.
 Proof.
   intros x n; elim n; simpl in |- *; auto with real.
-  intros H' H'0; elimtype False; omega.
+  intros H' H'0; exfalso; omega.
   intros n0; case n0.
   simpl in |- *; rewrite Rmult_1_r; auto.
   intros n1 H' H'0 H'1.
@@ -756,7 +756,7 @@ Proof.
   unfold R_dist in |- *; intros; split_Rabs; try ring.
   generalize (Ropp_gt_lt_0_contravar (y - x) r); intro;
     rewrite (Ropp_minus_distr y x) in H; generalize (Rlt_asym (x - y) 0 r0);
-      intro; unfold Rgt in H; elimtype False; auto.
+      intro; unfold Rgt in H; exfalso; auto.
   generalize (minus_Rge y x r); intro; generalize (minus_Rge x y r0); intro;
     generalize (Rge_antisym x y H0 H); intro; rewrite H1;
       ring.
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 810a7de03..be7895f5c 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -95,7 +95,7 @@ Proof.
   elim H0; intro.
   apply Req_le; assumption.
   clear H0; generalize (H r H1); intro; generalize (Rlt_irrefl r); intro;
-    elimtype False; auto.
+    exfalso; auto.
 Qed.
 
 (*********)
@@ -355,7 +355,7 @@ Proof.
   intro; generalize (prop_eps (- (l - l')) H1); intro;
     generalize (Ropp_gt_lt_0_contravar (l - l') r); intro;
       unfold Rgt in H3; generalize (Rgt_not_le (- (l - l')) 0 H3);
-        intro; elimtype False; auto.
+        intro; exfalso; auto.
   intros; cut (eps * / 2 > 0).
   intro; generalize (H0 (eps * / 2) H2); rewrite (Rmult_comm eps (/ 2));
     rewrite <- (Rmult_assoc 2 (/ 2) eps); rewrite (Rinv_r 2).
diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v
index d940a1d11..379d3495b 100644
--- a/theories/Reals/Rlogic.v
+++ b/theories/Reals/Rlogic.v
@@ -179,7 +179,7 @@ assert (Z:  Un_cv (fun N : nat => sum_f_R0 g N) ((1/2)^n)).
    simpl; unfold g;
    destruct (eq_nat_dec 0 n) as [t|f]; try reflexivity.
    elim f; auto with *.
-  elimtype False; omega.
+  exfalso; omega.
  destruct IHa as [IHa0 IHa1].
  split;
   intros H;
@@ -191,7 +191,7 @@ assert (Z:  Un_cv (fun N : nat => sum_f_R0 g N) ((1/2)^n)).
    ring_simplify.
    apply IHa0.
    omega.
-  elimtype False; omega.
+  exfalso; omega.
  ring_simplify.
  apply IHa1.
  omega.
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index 62f1940bf..33b7c8d1d 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -81,7 +81,7 @@ Section sequence.
   Proof.
     double induction n m; intros.
     unfold Rge in |- *; right; trivial.
-    elimtype False; unfold ge in H1; generalize (le_Sn_O n0); intro; auto.
+    exfalso; unfold ge in H1; generalize (le_Sn_O n0); intro; auto.
     cut (n0 >= 0)%nat.
     generalize H0; intros; unfold Un_growing in H0;
       apply
@@ -91,7 +91,7 @@ Section sequence.
     elim (lt_eq_lt_dec n1 n0); intro y.
     elim y; clear y; intro y.
     unfold ge in H2; generalize (le_not_lt n0 n1 (le_S_n n0 n1 H2)); intro;
-      elimtype False; auto.
+      exfalso; auto.
     rewrite y; unfold Rge in |- *; right; trivial.
     unfold ge in H0; generalize (H0 (S n0) H1 (lt_le_S n0 n1 y)); intro;
       unfold Un_growing in H1;
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 ->