test-suite/bugs/closed/bug_1680.v


1
2
3
4
5
6
7

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.