From e5b2cd1564296a9a7073615bcbf0ca7b9238d43d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 25 Sep 2015 11:58:51 -0700
Subject: [PATCH] refactor(library/blast): rename goal to branch

---
 src/library/blast/{goal.h => branch.h} | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)
 rename src/library/blast/{goal.h => branch.h} (84%)

diff --git a/src/library/blast/goal.h b/src/library/blast/branch.h
similarity index 84%
rename from src/library/blast/goal.h
rename to src/library/blast/branch.h
index 9d80f5e7f..49c69220b 100644
--- a/src/library/blast/goal.h
+++ b/src/library/blast/branch.h
@@ -11,13 +11,15 @@ Author: Leonardo de Moura
 
 namespace lean {
 namespace blast {
-class goal {
+typedef rb_tree<unsigned, unsigned_cmp> metavar_set;
+
+class branch {
     typedef rb_map<unsigned, hypothesis, unsigned_cmp> context;
     friend class state;
     unsigned      m_next;
     context       m_context;
-    expr          m_type;
-    expr const & mk_lref(expr const & type, optional<expr> const & value);
+    expr          m_target;
+    metavar_set   m_mvars;
 public:
     goal():m_next(0) {}
     hypothesis const * get(unsigned idx) const { return m_context.find(idx); }