blob: a9edcc8043f2ae282b24d859b50e0262ff5a5f30 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(** 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.
|
