From a104b478f3e4f864ce624bb7c18f1ff2120e44d6 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Wed, 4 Nov 2015 17:45:54 -0800 Subject: [PATCH] feat(library/type_context): make expand_macro public --- src/library/type_context.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/library/type_context.h b/src/library/type_context.h index 4964f9576..70e631693 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -147,7 +147,6 @@ class type_context { bool m_check_types; bool is_opaque(declaration const & d) const; - optional expand_macro(expr const & m); optional reduce_projection(expr const & e); optional norm_ext(expr const & e); expr whnf_core(expr const & e); @@ -378,6 +377,9 @@ public: bool has_assigned_uvar(levels const & ls) const; bool has_assigned_uvar_mvar(expr const & e) const; + /** \brief Expand macro using extension context */ + optional expand_macro(expr const & m); + /** \brief Instantiate assigned universe unification variables occurring in \c l */ level instantiate_uvars(level const & l);