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/Integer/Abstract/ZMulOrder.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/Numbers/Integer/Abstract')

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.
 
-- 
cgit v1.2.3