fix(library/local_context): bug in abstract_locals procedure

src/kernel/abstract.cpp

@@ -43,7 +43,7 @@ expr abstract_locals(expr const & e, unsigned n, expr const * subst) {
                     if (mlocal_name(subst[i]) == mlocal_name(m))
                         return some_expr(mk_var(offset + n - i - 1, m.get_tag()));
                 }
-                return some_expr(m);
+                return none_expr();
             }
             return none_expr();
         });

src/library/local_context.cpp

@@ -31,7 +31,7 @@ expr local_context::abstract_locals(expr const & e, list<expr> const & locals) {
                         return some_expr(copy_tag(m, mk_var(offset + i)));
                     i++;
                 }
-                return some_expr(m);
+                return none_expr();
             }
             return none_expr();
         });

tests/lean/run/local_ctx_bug.lean

@@ -0,0 +1,25 @@
+import data.finset data.finset.card data.finset.equiv
+open nat nat.finset decidable
+
+namespace finset
+variable {A : Type}
+open finset (to_nat)
+open finset (of_nat)
+
+private lemma of_nat_eq_insert : ∀ {n s : nat}, n ∉ of_nat s → of_nat (2^n + s) = insert n (of_nat s)
+| 0        s h := sorry
+| (succ n) s h :=
+  have n ∉ of_nat s,                     from sorry,
+  assert of_nat s = insert n (of_nat s), from sorry,
+  finset.ext (λ x,
+  have gen : ∀ m, m ∈ of_nat (2^(succ n) + s) ↔ m ∈ insert (succ n) (of_nat s)
+  | zero     :=
+    assert aux₁ : odd (2^(succ n) + s) ↔ odd s, from sorry,
+    calc
+      0 ∈ of_nat (2^(succ n) + s) ↔ odd (2^(succ n) + s)           : sorry
+                             ...  ↔ odd s                          : aux₁
+                             ...  ↔ 0 ∈ insert (succ n) (of_nat s) : sorry
+  | (succ m) := sorry,
+  gen x)
+
+end finset