mathlib
37e97b53 - feat(tactic): fix two bugs with generalize' (#3710)

Commit
5 years ago
feat(tactic): fix two bugs with generalize' (#3710) The name generated by `generalize'` will be exactly the given name, even if the name already occurs in the context. There was a bug with `generalize' h : e = x` if `e` occurred in the goal.
Author
Parents
Loading