From 2640d3085b4015153bb380b8326decd269cb0743 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 3 Feb 2017 14:04:59 -0800
Subject: [PATCH] fix(library/init/meta/interactive): name resolution problems
 in parametric sections

---
 library/init/meta/interactive.lean            |  6 ++--
 library/init/meta/smt/interactive.lean        |  6 ++--
 .../run/name_resolution_with_params_bug.lean  | 31 +++++++++++++++++++
 3 files changed, 35 insertions(+), 8 deletions(-)
 create mode 100644 tests/lean/run/name_resolution_with_params_bug.lean

diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 18dcf205fd..2ed42a8f7d 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -222,8 +222,7 @@ do {
   e ← resolve_name n,
   match e with
   | expr.const n _           := mk_const n -- create metavars for universe levels
-  | expr.local_const _ _ _ _ := return e
-  | _                        := report_resolve_name_failure e n
+  | _                        := return e
   end
 }
 
@@ -440,11 +439,10 @@ do
     (do eqns ← get_eqn_lemmas_for tt n, guard (eqns^.length > 0), save_const_type_info n ref, add_simps s eqns)
     <|>
     report_invalid_simp_lemma n
-  | expr.local_const _ _ _ _ :=
+  | _ :=
     (do b ← is_valid_simp_lemma reducible e, guard b, try (save_type_info e ref), s^.add e)
     <|>
     report_invalid_simp_lemma n
-  | _                        := report_resolve_name_failure e n
   end
 
 private meta def simp_lemmas.add_pexpr (s : simp_lemmas) (p : pexpr) : tactic simp_lemmas :=
diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean
index 65916f3312..53268d7ce6 100644
--- a/library/init/meta/smt/interactive.lean
+++ b/library/init/meta/smt/interactive.lean
@@ -137,8 +137,7 @@ do
   e ← resolve_name n,
   match e with
   | expr.const n _           := (add_ematch_lemma_from_decl_core md lhs_lemma n >> tactic.save_const_type_info n ref) <|> report_invalid_em_lemma n
-  | expr.local_const _ _ _ _ := (add_ematch_lemma_core md lhs_lemma e >> try (tactic.save_type_info e ref)) <|> report_invalid_em_lemma n
-  | _                        := tactic.report_resolve_name_failure e n
+  | _                        := (add_ematch_lemma_core md lhs_lemma e >> try (tactic.save_type_info e ref)) <|> report_invalid_em_lemma n
   end
 
 
@@ -185,11 +184,10 @@ do
     (do hs₁ ← mk_ematch_eqn_lemmas_for_core md n, tactic.save_const_type_info n ref, return $ hs^.merge hs₁)
     <|>
     report_invalid_em_lemma n
-  | expr.local_const _ _ _ _ :=
+  | _ :=
     (do h ← hinst_lemma.mk_core md e lhs_lemma, try (tactic.save_type_info e ref), return $ hs^.add h)
     <|>
     report_invalid_em_lemma n
-  | _                        := tactic.report_resolve_name_failure e n
   end
 
 private meta def add_hinst_lemma_from_pexpr (md : transparency) (lhs_lemma : bool) (p : pexpr) (hs : hinst_lemmas) : smt_tactic hinst_lemmas :=
diff --git a/tests/lean/run/name_resolution_with_params_bug.lean b/tests/lean/run/name_resolution_with_params_bug.lean
new file mode 100644
index 0000000000..e2a0542818
--- /dev/null
+++ b/tests/lean/run/name_resolution_with_params_bug.lean
@@ -0,0 +1,31 @@
+section
+
+  parameters x y : nat
+  def z := x + y
+
+  lemma h0 : z = y + x := add_comm _ _
+
+  open tactic
+
+  theorem foo₁ : z = y + x := -- doesn't work
+  begin
+   rw h0
+  end
+
+  theorem foo₂ : z = y + x := -- works
+  by do rewrite `h0
+
+
+  theorem foo₃ : z = y + x := -- doesn't work
+  by rewrite h0
+
+  theorem foo₄ : z = y + x := -- doesn't work
+  begin
+   simp [h0]
+  end
+
+  theorem foo₅ : z = y + x := -- doesn't work
+  begin [smt]
+    ematch_using [h0]
+  end
+end