From 88cccb19502dfec65f7e21d0f6772ba99b1fb99d Mon Sep 17 00:00:00 2001
From: Andrej Dudenhefner <31094379+mrhaandi@users.noreply.github.com>
Date: Thu, 8 Sep 2022 15:59:56 +0200
Subject: Improved auto goal selection (#443)

Improves robustness in case of stronger (e)auto.
This is in preparation of a change in Coq that will make auto and eauto stronger
(https://github.com/coq/coq/pull/16293).
---
 lib/Integers.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/Integers.v b/lib/Integers.v
index 10faeefa..b69e9842 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -1263,7 +1263,7 @@ Qed.
 
 Theorem and_zero: forall x, and x zero = zero.
 Proof.
-  bit_solve. apply andb_b_false.
+  bit_solve; apply andb_b_false.
 Qed.
 
 Corollary and_zero_l: forall x, and zero x = zero.
@@ -1273,7 +1273,7 @@ Qed.
 
 Theorem and_mone: forall x, and x mone = x.
 Proof.
-  bit_solve. apply andb_b_true.
+  bit_solve; apply andb_b_true.
 Qed.
 
 Corollary and_mone_l: forall x, and mone x = x.
-- 
cgit