fix(library/init/meta/interactive): name resolution problems in parametric sections

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 :=

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 :=

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