From c5db7f8dcf98fc354737ad15dc783c2e9241efb5 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Fri, 17 Sep 2021 18:13:27 +0200
Subject: Solve bug in prop2bool

---
 src/PropToBool.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/PropToBool.v b/src/PropToBool.v
index ec3b64c..cad6dae 100644
--- a/src/PropToBool.v
+++ b/src/PropToBool.v
@@ -50,7 +50,7 @@ Ltac prop2bool :=
       | bool =>
         lazymatch y with
         | true => fail
-        | _ => rewrite <- eqb_true_iff
+        | _ => rewrite <- (eqb_true_iff x y)
         end
       | _ =>
         lazymatch goal with
-- 
cgit