From 18808d133e1c418f2667d4d710d1d178193c70ae Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 6 Feb 2015 16:09:59 -0800
Subject: [PATCH] refactor(library/tactic/goal): move goal => local_context
 conversion to goal class

---
 src/library/tactic/goal.cpp           | 8 ++++++++
 src/library/tactic/goal.h             | 3 +++
 src/library/tactic/rewrite_tactic.cpp | 4 +---
 3 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp
index 60ad06a04..fb3791bff 100644
--- a/src/library/tactic/goal.cpp
+++ b/src/library/tactic/goal.cpp
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <utility>
+#include <algorithm>
 #include "util/buffer.h"
 #include "util/sstream.h"
 #include "util/sexpr/option_declarations.h"
@@ -34,6 +35,13 @@ bool get_pp_compact_goals(options const & o) {
     return o.get_bool(*g_pp_compact_goals, LEAN_DEFAULT_PP_COMPACT_GOALS);
 }
 
+local_context goal::to_local_context() const {
+    buffer<expr> hyps;
+    get_hyps(hyps);
+    std::reverse(hyps.begin(), hyps.end());
+    return local_context(to_list(hyps));
+}
+
 format goal::pp(formatter const & fmt) const {
     return pp(fmt, substitution());
 }
diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h
index 3bd06db2b..e64b65626 100644
--- a/src/library/tactic/goal.h
+++ b/src/library/tactic/goal.h
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "kernel/formatter.h"
 #include "kernel/environment.h"
 #include "library/io_state_stream.h"
+#include "library/local_context.h"
 
 namespace lean {
 /**
@@ -71,6 +72,8 @@ public:
     */
     list<expr> to_context() const;
 
+    local_context to_local_context() const;
+
     /** \brief Apply given substitution to goal */
     goal instantiate(substitution const & s) const;
 
diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp
index b816e3b04..64455c9da 100644
--- a/src/library/tactic/rewrite_tactic.cpp
+++ b/src/library/tactic/rewrite_tactic.cpp
@@ -472,9 +472,7 @@ class rewrite_fn {
 
     void update_goal(goal const & g) {
         m_g   = g;
-        buffer<expr> hyps;
-        g.get_hyps(hyps);
-        m_ctx = local_context(to_list(hyps));
+        m_ctx = m_g.to_local_context();
     }
 
     expr mk_meta(expr const & type) {