aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/1680.v
blob: 524c7bab42edcb2792081442bbc1a0783e25a037 (plain)
1
2
3
4
5
6
7
8
9
Ltac int1 := let h := fresh in intro h.

Goal nat -> nat -> True.
  let h' := fresh in (let h := fresh in intro h); intro h'.
  Restart. let h' := fresh in int1; intro h'.
  trivial.
Qed.