bug7191.v « output « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/output/bug7191.v

blob: 1aa4625b6c53c0e2f448fed8046f1ce6db65a6c8 (plain)

1
2
3

Require Extraction.
Definition f (x : False) : unit -> unit := match x with end.
Recursive Extraction f.