From 4e21c35b306bae7d832e6d0c0758069856b144b7 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 21 Sep 2016 13:42:58 +0200 Subject: The contradiction tactic has become more powerful. --- flocq/Core/Fcore_digits.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'flocq') diff --git a/flocq/Core/Fcore_digits.v b/flocq/Core/Fcore_digits.v index d40c1a09..7d1d490a 100644 --- a/flocq/Core/Fcore_digits.v +++ b/flocq/Core/Fcore_digits.v @@ -853,8 +853,7 @@ Proof. intros n Zn. rewrite <- (Zdigits_abs n). assert (Hn: (0 < Zabs n)%Z). -destruct n ; try easy. -now elim Zn. +destruct n ; now easy. destruct (Zabs n) as [|p|p] ; try easy ; clear. simpl. generalize 1%Z (radix_val beta) (refl_equal Lt : (0 < 1)%Z). -- cgit