fix(frontends/lean/definition_cmds): set scope_pos_info when checking…

… examples
leanprover · Feb 25, 2017 · fcc0f30 · fcc0f30
1 parent 04e27eb
commit fcc0f30
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
@@ -741,6 +741,7 @@ class example_checking_task : public task<unit> {
         scope_trace_env scope2(m_decl_env, m_opts, *tc);
         scope_pos_info_provider scope3(m_pos_provider);
         auto_reporting_info_manager_scope scope4(get_module_id(), m_use_info_manager);
+        module::scope_pos_info scope_pos(m_pos_provider.get_some_pos());
 
         name decl_name = "_example";