The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Hello.

Is it possible to configure extraction such way that all modules will be eliminated from extracted code and parameters of them will be replaced with explicit extra arguments to functions?

E.g. this:

Module Type T.

Parameter P : Set.

End M.

(* In one file: *)

Module N := T nat. Import N.

Definition f : P := 1.
(* In other file: *)

Module B := T bool. Import N.

Definition f : P := true.

must become this:

(* In one file: *)

Definition f : nat := 1.
(* In other file: *)

Definition f : bool := true.

Sincerely,
Kirill Taran