From a14865049571f157896107ebf0b2f908b1b95cbc Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 7 Jun 2021 22:45:39 +0200
Subject: coq 8.13.2

---
 lib/Integers.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/Integers.v b/lib/Integers.v
index 3e103ab7..2addc78b 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -3747,8 +3747,7 @@ Proof.
     unfold lt.
     rewrite signed_zero.
     rewrite bits_zero.
-    destruct (zlt _ _); try lia.
-    reflexivity.
+    destruct (zlt _ _); try lia; reflexivity.
   }
   change (Z.testbit (unsigned x) (i + 63)) with (testbit x (i + 63)).
   rewrite bits_zero.
-- 
cgit