From bb759b1a90052fbdb4e57bfb1dfee61abd57bbb0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 11 Jan 2016 11:59:54 -0800
Subject: [PATCH] feat(library/blast/congruence_closure): use blast.cc.heq by
 default

---
 src/library/blast/congruence_closure.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp
index 62034786a7..47aaaa42ff 100644
--- a/src/library/blast/congruence_closure.cpp
+++ b/src/library/blast/congruence_closure.cpp
@@ -18,11 +18,11 @@ Author: Leonardo de Moura
 #include "library/blast/options.h"
 
 #ifndef LEAN_DEFAULT_BLAST_CC_HEQ
-#define LEAN_DEFAULT_BLAST_CC_HEQ false
+#define LEAN_DEFAULT_BLAST_CC_HEQ true
 #endif
 
 #ifndef LEAN_DEFAULT_BLAST_CC_SUBSINGLETON
-#define LEAN_DEFAULT_BLAST_CC_SUBSINGLETON false
+#define LEAN_DEFAULT_BLAST_CC_SUBSINGLETON true
 #endif
 
 namespace lean {