From 3bb09e9959a4aeaaab8138fc5edfcee08dbd06c5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 6 Oct 2015 08:35:24 -0700
Subject: [PATCH] fix(library/blast): typos

---
 src/library/blast/blast.cpp      | 2 +-
 src/library/blast/infer_type.cpp | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp
index 8bed5e13a9..0ca4274de2 100644
--- a/src/library/blast/blast.cpp
+++ b/src/library/blast/blast.cpp
@@ -66,7 +66,7 @@ class blastenv {
             lean_unreachable();
         }
 
-        expr visit_sort(expr const & e) {
+        virtual expr visit_sort(expr const & e) {
             return blast::mk_sort(to_blast_level(sort_level(e)));
         }
 
diff --git a/src/library/blast/infer_type.cpp b/src/library/blast/infer_type.cpp
index ede0eea420..d4d99acc2e 100644
--- a/src/library/blast/infer_type.cpp
+++ b/src/library/blast/infer_type.cpp
@@ -338,7 +338,7 @@ static bool assign_mref_core(expr const & ma, expr const & v) {
     //   3. Any local constant occurring in new_v occurs in locals
     //   4. m does not occur in new_v
     bool ok = true;
-    for_each(v, [&](expr const & e, unsigned) {
+    for_each(new_v, [&](expr const & e, unsigned) {
             if (!ok)
                 return false; // stop search
             if (is_href(e)) {