From 1935986f3caaebd76e066d777895f2bd3550bf00 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 16 Mar 2019 18:41:58 -0700 Subject: [PATCH] fix(library/compiler/compiler): we must compile (non external) opaque constants --- src/library/compiler/compiler.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp index e27b6f7393..fa9f2acccc 100644 --- a/src/library/compiler/compiler.cpp +++ b/src/library/compiler/compiler.cpp @@ -171,7 +171,7 @@ environment compile(environment const & env, options const & opts, names cs) { for (name const & c : cs) { lean_assert(!is_extern_constant(env, c)); - if (!env.get(c).is_definition() || has_synthetic_sorry(env.get(c).get_value())) { + if ((!env.get(c).is_definition() && !env.get(c).is_opaque()) || has_synthetic_sorry(env.get(c).get_value())) { return env; } }