From 8048cbd6f27ac36947e9b141bfdb791cd6278814 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 28 Jul 2015 16:49:52 -0700
Subject: [PATCH] feat(kernel): do not hide semi-constructive axioms

---
 src/kernel/hits/hits.cpp         | 4 +---
 src/kernel/quotient/quotient.cpp | 3 +--
 2 files changed, 2 insertions(+), 5 deletions(-)

diff --git a/src/kernel/hits/hits.cpp b/src/kernel/hits/hits.cpp
index 550a82aa27..aec5fb4292 100644
--- a/src/kernel/hits/hits.cpp
+++ b/src/kernel/hits/hits.cpp
@@ -142,10 +142,8 @@ bool is_hits_decl(environment const & env, name const & n) {
         return false;
     return
         n == *g_trunc || n == *g_trunc_tr || n == *g_trunc_rec ||
-        n == *g_trunc_is_trunc_trunc ||
         n == *g_hit_quotient || n == *g_hit_quotient_class_of ||
-        n == *g_hit_quotient_rec || n == *g_hit_quotient_eq_of_rel ||
-        n == *g_hit_quotient_rec_eq_of_rel;
+        n == *g_hit_quotient_rec;
 }
 
 void initialize_hits_module() {
diff --git a/src/kernel/quotient/quotient.cpp b/src/kernel/quotient/quotient.cpp
index e284ca71c5..649bf2deea 100644
--- a/src/kernel/quotient/quotient.cpp
+++ b/src/kernel/quotient/quotient.cpp
@@ -133,8 +133,7 @@ bool is_quotient_decl(environment const & env, name const & n) {
     if (!get_extension(env).m_initialized)
         return false;
     return
-        n == *g_propext || n == *g_quotient || n == *g_quotient_lift || n == *g_quotient_ind || n == *g_quotient_mk ||
-        n == *g_quotient_sound;
+        n == *g_quotient || n == *g_quotient_lift || n == *g_quotient_ind || n == *g_quotient_mk;
 }
 
 void initialize_quotient_module() {