test-suite/bugs/closed/shouldsucceed/1680.v


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.