Revert "fix(tactic/resolve_constant): parameters are no longer a pr…

…oblem" This reverts commit b9d03a1.
leanprover-community · Sep 6, 2020 · 78daacb · 78daacb
1 parent b9d03a1
commit 78daacb
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 20 deletions.
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
@@ -896,16 +896,8 @@ 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,
-     pure $ e.get_app_fn.const_name
-   end
+do (expr.const n _) ← resolve_name n,
+   pure n
 
 meta def to_expr_strict (q : pexpr) : tactic expr :=
 to_expr q

diff --git a/tests/lean/run/resolve_name_bug.lean b/tests/lean/run/resolve_name_bug.lean
@@ -25,13 +25,3 @@ by simp [f_lemma1, f_lemma2]
 
 end bla
 end foo
-
-section param
-
-parameters x y : ℤ
-
-lemma my_ext (s s' : set ℤ) (h : x ∈ s ↔ y ∈ s') : true := trivial
-
-run_cmd tactic.resolve_constant `my_ext
-
-end param