The Coq mailing list

[Leonardo Rodriguez <leonardomatiasrodriguez AT gmail.com>]

Hi Coq Club,

Suppose you have some goal like this

H0 : P

H1 : Q

t1 := first_term : A

t2 := second_term : A

t3 := third_term : A

t4 := fourth_term t3 : A
==============

my_type t1 t2 = t4

I want to clean every [t_i] and replace the conclusion
with

my_type (first_term) (second_term) = fourth_term third_term

I'm trying to avoid doing:

unfold t1

unfold t2

unfold t3 in *

unfold t4

I don't know too much Ltac, but I tried to do

repeat match goal with

  [H : _ |- _] =>

    try unfold H

end

and it seems not to match with local variables.

Thank you!