The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

Hi,

Is [Parameter Inline] what you're looking for?

Regards, Rui Baptista

On Fri, Feb 21, 2014 at 12:56 PM, Kirill Taran <kirill.t256 AT gmail.com> wrote:

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