From e33bd2e66581287518f3ed32c7b011a59926b171 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 29 Dec 2016 16:18:13 -0800
Subject: [PATCH] chore(library/unfold_macros): checking whether commit
 7f86ad64eb9d5 broke the remote build

---
 src/library/tactic/ac_tactics.h | 3 +--
 src/library/unfold_macros.cpp   | 2 +-
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/library/tactic/ac_tactics.h b/src/library/tactic/ac_tactics.h
index 6abba8093d..58a8596e32 100644
--- a/src/library/tactic/ac_tactics.h
+++ b/src/library/tactic/ac_tactics.h
@@ -7,8 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "library/type_context.h"
 
-/* TODO(Leo): reduce after testing */
-#define LEAN_AC_MACROS_TRUST_LEVEL 10000000
+#define LEAN_AC_MACROS_TRUST_LEVEL 10
 
 namespace lean {
 class ac_manager {
diff --git a/src/library/unfold_macros.cpp b/src/library/unfold_macros.cpp
index 962ffae858..f7ae7099fe 100644
--- a/src/library/unfold_macros.cpp
+++ b/src/library/unfold_macros.cpp
@@ -18,7 +18,7 @@ Author: Leonardo de Moura
 /* If the trust level of all macros is < LEAN_BELIEVER_TRUST_LEVEL,
    then we skip the unfold_untrusted_macros potentially expensive step.
    The following definition is commented because we are currently testing the AC macros. */
-// #define LEAN_ALL_MACROS_HAVE_SMALL_TRUST_LVL
+#define LEAN_ALL_MACROS_HAVE_SMALL_TRUST_LVL
 
 namespace lean {
 class unfold_untrusted_macros_fn {