From 15f270d9f3fcb3190f63d29d8698c54346bb48c9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 29 Jun 2014 11:07:06 -0700
Subject: [PATCH] fix(library/tactic): memory leak that only happens when
 compiling with clang++

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/tactic/proof_state.cpp | 2 +-
 src/library/tactic/proof_state.h   | 2 +-
 src/library/tactic/tactic.cpp      | 4 ++--
 src/library/tactic/tactic.h        | 8 ++++----
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp
index bb62a393f..6169a9299 100644
--- a/src/library/tactic/proof_state.cpp
+++ b/src/library/tactic/proof_state.cpp
@@ -69,7 +69,7 @@ format proof_state::pp(environment const & env, formatter const & fmt, options c
     return r;
 }
 
-goals map_goals(proof_state const & s, std::function<optional<goal>(name const & gn, goal const & g)> const & f) {
+goals map_goals(proof_state const & s, std::function<optional<goal>(name const & gn, goal const & g)> f) {
     return map_filter(s.get_goals(), [=](std::pair<name, goal> const & in, std::pair<name, goal> & out) -> bool {
             check_interrupted();
             optional<goal> new_goal = f(in.first, in.second);
diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h
index 14aa6e46b..0d0b08e6e 100644
--- a/src/library/tactic/proof_state.h
+++ b/src/library/tactic/proof_state.h
@@ -80,7 +80,7 @@ proof_state to_proof_state(environment const & env, expr const & mvar, options c
 /** \brief Try to extract a proof from the given proof state */
 optional<expr> to_proof(proof_state const & s);
 
-goals map_goals(proof_state const & s, std::function<optional<goal>(name const & gn, goal const & g)> const & f);
+goals map_goals(proof_state const & s, std::function<optional<goal>(name const & gn, goal const & g)> f);
 io_state_stream const & operator<<(io_state_stream const & out, proof_state const & s);
 
 UDATA_DEFS_CORE(goals)
diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index 8d555d31a..1759ae2b1 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -18,7 +18,7 @@ Author: Leonardo de Moura
 #include "library/io_state_stream.h"
 
 namespace lean {
-tactic tactic01(std::function<optional<proof_state>(environment const &, io_state const & ios, proof_state const &)> const & f) {
+tactic tactic01(std::function<optional<proof_state>(environment const &, io_state const & ios, proof_state const &)> f) {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
             return mk_proof_state_seq([=]() {
                     auto r = f(env, ios, s);
@@ -30,7 +30,7 @@ tactic tactic01(std::function<optional<proof_state>(environment const &, io_stat
         });
 }
 
-tactic tactic1(std::function<proof_state(environment const &, io_state const & ios, proof_state const &)> const & f) {
+tactic tactic1(std::function<proof_state(environment const &, io_state const & ios, proof_state const &)> f) {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
             return mk_proof_state_seq([=]() {
                     auto r = f(env, ios, s);
diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h
index ef1f61361..c5a612bb6 100644
--- a/src/library/tactic/tactic.h
+++ b/src/library/tactic/tactic.h
@@ -24,8 +24,8 @@ inline optional<tactic> some_tactic(tactic && t) { return optional<tactic>(std::
 
 template<typename F> inline proof_state_seq mk_proof_state_seq(F && f) { return mk_lazy_list<proof_state>(std::forward<F>(f)); }
 
-tactic tactic01(std::function<optional<proof_state>(environment const &, io_state const & ios, proof_state const &)> const & f);
-tactic tactic1(std::function<proof_state(environment const &, io_state const & ios, proof_state const &)> const & f);
+tactic tactic01(std::function<optional<proof_state>(environment const &, io_state const & ios, proof_state const &)> f);
+tactic tactic1(std::function<proof_state(environment const &, io_state const & ios, proof_state const &)> f);
 
 /** \brief Return a "do nothing" tactic (aka skip). */
 tactic id_tactic();
@@ -115,9 +115,9 @@ typedef std::function<bool(environment const & env, io_state const & ios, proof_
     \brief Return a tactic that applies the predicate \c p to the input state.
     If \c p returns true, then applies \c t1. Otherwise, applies \c t2.
 */
-tactic cond(proof_state_pred const & p, tactic const & t1, tactic const & t2);
+tactic cond(proof_state_pred p, tactic const & t1, tactic const & t2);
 /** \brief Syntax-sugar for cond(p, t, id_tactic()) */
-inline tactic when(proof_state_pred const & p, tactic const & t) { return cond(p, t, id_tactic()); }
+inline tactic when(proof_state_pred p, tactic const & t) { return cond(p, t, id_tactic()); }
 /**
    \brief Return a tactic that applies \c t only to the goal named \c gname.
    The tactic fails if the input state does not have a goal named \c gname.