The Coq mailing list

[David Pichardie <david.pichardie AT irisa.fr>]

Hi,

Is there a simple way in Coq to simulate the ocaml include command ?

The only solution, I found for the moment is to copy all definitions.

Example :

Module Type SIG.

Parameter A : Set.
Parameter a1 a2 : A.

End SIG.

Module F (M:SIG) <: SIG.

Definition A := M.A.    (************************)
Definition a1 := M.a1.  (*     instead of include M      *)
Definition a2 := M.a2.  (************************)

(* ... *)

End F.