Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
bug_4709.v
Sprache: Unknown
(** Bug 4709 https://coq.inria.fr/bug/4709
Extraction wasn't reducing primitive projections in types. *)
Require Extraction.
Set Primitive Projections.
Record t := Foo { foo : Type }.
Definition ty := foo (Foo nat).
(* Without proper reduction of primitive projections in
[extract_type], the type [ty] was extracted as [Tunknown].
Let's check it isn't the case anymore. *)
Parameter check : nat.
Extract Constant check => "(O:ty)".
Extraction TestCompile ty check.
[ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
]
|