From 80cd98c6fcae2ad4939504163c1cf10c80dcbfb3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 18 Dec 2019 11:25:17 +0100
Subject: [PATCH] [qed] merge terms with type Bool and Prop
---
src/plugins/qed/term.ml | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index f2015ffb1c5..b759702b9a3 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -235,6 +235,7 @@ struct
match t1, t2 with
| None, None -> true
| None, Some _ | Some _ , None -> false
+ | Some (Bool|Prop) , Some(Bool|Prop) -> true
| Some t1, Some t2 -> Tau.equal t1 t2
let sort x = x.sort
--
GitLab