summaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened/3320.v
blob: 05cf73281d29bbb1cc0547bb6282f629d3400ccd (plain)
1
2
3
4
Goal forall x : nat, True.
  fix 1.
  assumption.
Fail Qed.