From 93b74b4be215bd08ca7a123505177d6ec8ac7b4c Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 8 Oct 2009 13:39:01 +0000 Subject: 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 --- theories/Numbers/Natural/Abstract/NBase.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/Numbers/Natural/Abstract/NBase.v') 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. -- cgit v1.2.3