fix(tactic/resolve_constant): parameters are no longer a problem (#462

)

Moved PR from leanprover-community/mathlib3#4032

library/init/meta/tactic.lean

@@ -896,8 +896,14 @@ meta def intron_with
 
 /-- Returns n fully qualified if it refers to a constant, or else fails. -/
 meta def resolve_constant (n : name) : tactic name :=
-do (expr.const n _) ← resolve_name n,
-   pure n
+do e ← resolve_name n,
+   match e with
+   | expr.const n _ := pure n
+   | _ := do
+     e ← to_expr e tt ff,
+     expr.const n _ ← pure $ e.get_app_fn,
+     pure n
+   end
 
 meta def to_expr_strict (q : pexpr) : tactic expr :=
 to_expr q

tests/lean/run/resolve_name_bug.lean

@@ -25,3 +25,17 @@ by simp [f_lemma1, f_lemma2]
 
 end bla
 end foo
+
+section param
+
+parameters x y : ℤ
+
+lemma foo.my_ext (s s' : set ℤ) (h : x ∈ s ↔ y ∈ s') : true := trivial
+
+open foo
+
+run_cmd do
+n ← tactic.resolve_constant `my_ext,
+guard $ n = `foo.my_ext
+
+end param