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 {