michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/match): memory leak that only happens with compiling with clang++

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-26 10:24:38 -07:00
parent 631ebc6c4b
commit 9928390605
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/match.cpp
View file

@ -352,7 +352,7 @@ bool match(expr const & p, expr const & t, buffer<optional<expr>> & esubst, buff
return match_fn(esubst, lsubst, name_generator(*g_tmp_prefix), name_subst, plugin).match(p, t); return match_fn(esubst, lsubst, name_generator(*g_tmp_prefix), name_subst, plugin).match(p, t);
} }
match_plugin mk_whnf_match_plugin(std::shared_ptr<type_checker> const & tc) { match_plugin mk_whnf_match_plugin(std::shared_ptr<type_checker> tc) {
return [=](expr const & p, expr const & t, match_context & ctx) { // NOLINT return [=](expr const & p, expr const & t, match_context & ctx) { // NOLINT
try { try {
constraint_seq cs; constraint_seq cs;

2
src/library/match.h
View file

@ -49,7 +49,7 @@ public:
typedef std::function<bool(expr const &, expr const &, match_context &)> match_plugin; // NOLINT typedef std::function<bool(expr const &, expr const &, match_context &)> match_plugin; // NOLINT
/** \brief Create a match_plugin that puts terms in weak-head-normal-form before failing */ /** \brief Create a match_plugin that puts terms in weak-head-normal-form before failing */
match_plugin mk_whnf_match_plugin(std::shared_ptr<type_checker> const & tc); match_plugin mk_whnf_match_plugin(std::shared_ptr<type_checker> tc);
/** /**
\brief Matching for higher-order patterns. Return true iff \c t matches the higher-order pattern \c p. \brief Matching for higher-order patterns. Return true iff \c t matches the higher-order pattern \c p.