bug_4325.v « closed « bugs « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/bugs/closed/bug_4325.v

blob: de3e4bfa8c5936d39f7c56f140ca5efb99430045 (plain)

Goal (forall a b : nat, Set = (a = b)) -> Set.
Proof.
  clear.
  intro H.
  erewrite (fun H' => H _ H').
Abort.