Skip to content

Commit

Permalink
fix(tactic/h_generalize): fix name resolution in h_generalize
Browse files Browse the repository at this point in the history
  • Loading branch information
cipher1024 committed Feb 5, 2019
1 parent 178c09d commit ff5af10
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/tactic/interactive.lean
Original file line number Diff line number Diff line change
Expand Up @@ -490,7 +490,7 @@ meta def return_cast (f : option expr) (t : option (expr × expr))
(do guard (¬ e.has_var),
unify x x',
u ← mk_meta_univ,
f ← f <|> to_expr ``(@id %%(expr.sort u : expr)),
f ← f <|> mk_mapp ``_root_.id [(expr.sort u : expr)],
t' ← infer_type e,
some (f',t) ← pure t | return (some (f,t'), (e,x',eq_h) :: es),
infer_type e >>= is_def_eq t,
Expand Down

0 comments on commit ff5af10

Please sign in to comment.