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

about summary refs log tree commit diff

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

blob: 4d0e435df71e5b84eefa6612388cb089f5927728 (plain)

Require Extraction.

Primitive array := #array_type.

Definition a : array nat := [| 0%nat | 0%nat |].
Extraction a.