fix(library/type_context): bug introduced at d85c30f

Kha · May 9, 2018 · f8cedb3 · f8cedb3
1 parent d05e93f
commit f8cedb3
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
@@ -1989,7 +1989,7 @@ bool type_context_old::process_assignment(expr const & m, expr const & v) {
            This change is consistent with the general approach used in the rest of the code
            base where spurious typing errors due reducibility are avoided by using
            relaxed_is_def_eq. */
-        relaxed_scope _(*this);
+        relaxed_scope _(*this, transparency_mode::Semireducible);
         if (!is_def_eq_core(t1, t2)) {
             lean_trace(name({"type_context", "is_def_eq_detail"}),
                        scope_trace_env scope(env(), *this);

diff --git a/src/library/type_context.h b/src/library/type_context.h
@@ -794,8 +794,8 @@ class type_context_old : public abstract_type_context {
     struct relaxed_scope {
         transparency_scope m_transparency_scope;
         zeta_scope         m_zeta_scope;
-        relaxed_scope(type_context_old & ctx):
-            m_transparency_scope(ctx, transparency_mode::Semireducible),
+        relaxed_scope(type_context_old & ctx, transparency_mode m = transparency_mode::All):
+            m_transparency_scope(ctx, m),
             m_zeta_scope(ctx, true) {}
     };