a tactic to forget the definition

Stream: general

[Kenny Lau]

Can we make a tactic to forget the definition of something in the local context while keeping everything else unchanged?

[Kenny Lau]

so it would make h : R := 1+1 into h : R

[Chris Hughes]

Use generalize instead of let to define h in the first place. Is this something to do with trying to get subst to work?

[Kenny Lau]

it isn't

[Mario Carneiro]

you could replace h := h I think