The Coq mailing list

[Erik Martin-Dorel <e.mdorel AT gmail.com>]

Dear Coq developers,

When playing with modules in Coq, I have noticed a distracting
limitation of the [Include] vernacular:

First, let us define a module type such as

(* ---------------- 8< ---------------- *)
Module Type MT.
Parameters t1 t2 : Type.
Definition t := t1 -> t2.
End MT.
(* ---------------- 8< ---------------- *)

Then suppose you want to deal with module type expressions such as
[MT with Definition t1 := nat with Definition t2 := bool].

The following is not accepted by Coq 8.4pl1:

(* ---------------- 8< ---------------- *)
Module M <: MT.
Include MT with Definition t1 := nat with Definition t2 := bool.
(* Fails with "Syntax error: '.' expected after [...]" *)
End M.
(* ---------------- 8< ---------------- *)

Yet, the vernacular command [Include Type] that Hugo was mentioning in
<https://sympa.inria.fr/sympa/arc/coq-club/2008-09/msg00071.html>
works in this context (despite the fact that it raises the "Warning:
Include Type is deprecated; use Include instead"):

(* ---------------- 8< ---------------- *)
(* Workaround 1 *)
Module M <: MT.
Include Type MT with Definition t1 := nat with Definition t2 := bool.

(* Succeeds with a warning *)

End M.
(* ---------------- 8< ---------------- *)

As another workaround, we can also write something such as the
following, but it is a bit less satisfactory since we need to define
an additional module type:

(* ---------------- 8< ---------------- *)
(* Workaround 2 *)
Module Type MT' := MT with Definition t1 := nat with Definition t2 := bool.
Module M' <: MT.
Include MT'.
End M'.
(* ---------------- 8< ---------------- *)

So my question: Would it be feasible to implement the syntax
[Include module_type with Definition qualid := term]
in next releases of Coq?

(I guess this also concerns the syntax
[Include module_type with Module qualid := qualid]).

Kind regards,

Erik

--

Érik Martin-Dorel

http://erik.martin-dorel.org/