From 34acf2003c510ec06baf00a6a63a6d2c6cffd64d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 25 Oct 2019 10:44:42 -0700
Subject: [PATCH] chore: rename `assign` delayed method

---
 src/library/metavar_context.cpp     | 4 ++--
 src/library/metavar_context.h       | 2 +-
 src/library/tactic/intro_tactic.cpp | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/library/metavar_context.cpp b/src/library/metavar_context.cpp
index d373973512..c044c6e247 100644
--- a/src/library/metavar_context.cpp
+++ b/src/library/metavar_context.cpp
@@ -139,7 +139,7 @@ void metavar_context::assign(expr const & e, expr const & v) {
     lean_assert(is_assigned(e));
 }
 
-void metavar_context::assign(expr const & e, local_context const & lctx, exprs const & locals, expr const & v) {
+void metavar_context::assign_delayed(expr const & e, local_context const & lctx, exprs const & locals, expr const & v) {
     m_obj = lean_metavar_ctx_assign_delayed(m_obj, mvar_name(e).to_obj_arg(), lctx.to_obj_arg(), locals.to_obj_arg(), v.to_obj_arg());
     lean_assert(is_delayed_assigned(e));
 }
@@ -187,7 +187,7 @@ struct metavar_context::interface_impl {
         if (has_expr_metavar(new_v)) {
             m_delayed_found.insert(mvar_name(e));
             if (!is_eqp(new_v, d->get_val()))
-                m_ctx.assign(e, d->get_lctx(), d->get_locals(), new_v);
+                m_ctx.assign_delayed(e, d->get_lctx(), d->get_locals(), new_v);
             return none_expr();
         } else {
             m_ctx.m_obj = lean_metavar_ctx_erase_delayed(m_ctx.m_obj, mvar_name(e).to_obj_arg());
diff --git a/src/library/metavar_context.h b/src/library/metavar_context.h
index ed32077f0d..6c02597aef 100644
--- a/src/library/metavar_context.h
+++ b/src/library/metavar_context.h
@@ -99,7 +99,7 @@ public:
 
       \pre is_metavar_decl_ref(e)
     */
-    void assign(expr const & e, local_context const & lctx, exprs const & locals, expr const & v);
+    void assign_delayed(expr const & e, local_context const & lctx, exprs const & locals, expr const & v);
 
     level instantiate_mvars(level const & l);
     expr instantiate_mvars(expr const & e);
diff --git a/src/library/tactic/intro_tactic.cpp b/src/library/tactic/intro_tactic.cpp
index a4d985cace..15d868b0a8 100644
--- a/src/library/tactic/intro_tactic.cpp
+++ b/src/library/tactic/intro_tactic.cpp
@@ -46,7 +46,7 @@ optional<expr> intron_core(environment const & env, options const & opts, metava
     }
     expr new_M   = ctx.mk_metavar_decl(ctx.lctx(), type);
     mctx = ctx.mctx();
-    mctx.assign(mvar, ctx.lctx(), exprs(new_Hs), new_M);
+    mctx.assign_delayed(mvar, ctx.lctx(), exprs(new_Hs), new_M);
     return some_expr(new_M);
 }