diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-08 13:39:01 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-08 13:39:01 +0000 |
| commit | 93b74b4be215bd08ca7a123505177d6ec8ac7b4c (patch) | |
| tree | cc5b80a8ba038a7c531afae977234f2afdc70699 /theories/Numbers/Integer | |
| parent | bdec9fddcdaa13800e04e718ffa52f87bddc52d9 (diff) | |
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
Diffstat (limited to 'theories/Numbers/Integer')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZMulOrder.v | 4 |
1 files changed, 2 insertions, 2 deletions
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. |