refactor(local_context): local_context::scope auxiliary object is not

needed anymore

src/frontends/lean/elaborator.cpp

@@ -99,13 +99,6 @@ class elaborator : public coercion_info_manager {
     info_manager         m_pre_info_data;
     unifier_config       m_unifier_config;
 
-    struct scope_ctx {
-        elaborator &         m_main;
-        local_context::scope m_scope1;
-        local_context::scope m_scope2;
-        scope_ctx(elaborator & e):m_main(e), m_scope1(e.m_context), m_scope2(e.m_full_context) {}
-    };
-
     /** \brief Set local context for the given metavariable application */
     void set_local_context_for(expr const & meta) {
         lean_assert(is_meta(meta));
@@ -701,7 +694,8 @@ public:
     }
 
     expr visit_binding(expr e, expr_kind k, constraint_seq & cs) {
-        scope_ctx scope(*this);
+        flet<local_context> save1(m_context, m_context);
+        flet<local_context> save2(m_full_context, m_full_context);
         buffer<expr> ds, ls, es;
         while (e.kind() == k) {
             es.push_back(e);

src/frontends/lean/local_context.cpp

@@ -105,11 +105,4 @@ void local_context::add_local(expr const & l) {
 list<expr> const & local_context::get_data() const {
     return m_ctx;
 }
-
-local_context::scope::scope(local_context & main):
-    m_main(main), m_old_ctx(main.m_ctx), m_old_ctx_abstracted(main.m_ctx_abstracted) {}
-local_context::scope::~scope() {
-    m_main.m_ctx            = m_old_ctx;
-    m_main.m_ctx_abstracted = m_old_ctx_abstracted;
-}
 }

src/frontends/lean/local_context.h

@@ -77,15 +77,5 @@ public:
     list<expr> const & get_data() const;
 
     void add_local(expr const & l);
-
-    /** \brief Scope object for restoring the content of the context */
-    class scope {
-        local_context & m_main;
-        list<expr>      m_old_ctx;
-        list<expr>      m_old_ctx_abstracted;
-    public:
-        scope(local_context & main);
-        ~scope();
-    };
 };
 }

src/frontends/lean/placeholder_elaborator.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/lazy_list_fn.h"
+#include "util/flet.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
 #include "library/unifier.h"
@@ -103,7 +104,7 @@ struct placeholder_elaborator : public choice_iterator {
         tag g                 = inst.get_tag();
         local_context & ctx   = m_C->m_ctx;
         try {
-            local_context::scope scope(ctx);
+            flet<local_context> scope(ctx, ctx);
             buffer<expr> locals;
             expr meta_type = m_meta_type;
             while (true) {