The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Hi, all;
I would like to know what is the reason why the following code:

>Record foo : Type := {bar:forall (A:Set), A -> A; foobar:nat}.
>Definition id : foo := {|bar := fun A a => a; foobar := 0|}.
>
>Recursive Extraction id.

is extracted to:

>>type __ = Obj.t
>>
>>type nat =
>>| O
>>| S of nat
>>
>>type foo = { bar : (__ -> __ -> __); foobar : nat }
>>
>>(** val id : foo **)
>>
>>let id =
>>  { bar = (fun _ a -> a); foobar = O }

and not

>>type nat =
>>| O
>>| S of nat
>>
>>type foo = { bar : ('a. 'a -> 'a); foobar : nat }
>>
>>(** val id : foo **)
>>
>>let id =
>>  { bar = (fun _ a -> a); foobar = O }

More precisely, I would like to know if there is a way to have nice
"'a.…" instead of ugly "__ ->…".

I guess I can hack to have it, but if there are good reasons for not
having it maybe I should leave it as it is.