From 2cb018734eedc773c31d5e8772be778b663aceb6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Feb 2018 10:13:19 -0800 Subject: [PATCH] chore(library/metavar_context): add TODO's --- src/library/metavar_context.cpp | 2 ++ src/library/metavar_context.h | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/library/metavar_context.cpp b/src/library/metavar_context.cpp index 0cc64568c3..d70f959fbc 100644 --- a/src/library/metavar_context.cpp +++ b/src/library/metavar_context.cpp @@ -53,10 +53,12 @@ static name mk_meta_decl_name() { } level metavar_context::mk_univ_metavar_decl() { + // TODO(Leo): use m_ngen.next() instead of mk_meta_decl_name return mk_meta_univ(mk_meta_decl_name()); } expr metavar_context::mk_metavar_decl(optional const & pp_n, local_context const & ctx, expr const & type) { + // TODO(Leo): use m_ngen.next() instead of mk_meta_decl_name name n = mk_meta_decl_name(); m_decls.insert(n, metavar_decl(ctx, head_beta_reduce(type))); return mk_meta_ref(n, pp_n); diff --git a/src/library/metavar_context.h b/src/library/metavar_context.h index 43ef0920ca..a534bdc3ba 100644 --- a/src/library/metavar_context.h +++ b/src/library/metavar_context.h @@ -30,7 +30,7 @@ class metavar_context { name_map m_decls; name_map m_uassignment; name_map m_eassignment; - name_generator m_ngen; + name_generator m_ngen; // TODO(Leo): this field is not being used yet. struct interface_impl; friend struct interface_impl;