It is surprising for me to see that Coq can Include a functor and will instantiate it with the current interactive module.
Coq Ref Manual:
Command Include module_type_inl <+ module_expr_inl*
Includes the content of module(s) in the current interactive module. Here module_type_inl can be a module expression or a module type expression. If it is a high-order module or module type expression then the system tries to instantiate module_type_inl with the current interactive module.
A working example:
Module Type B.
Parameter b : Set.
End B.
Module A (ctx : B).
Definition a : ctx.b -> ctx.b := fun x => x.
End A.
Module SeeHere.
Definition b := nat.
Include A.
End SeeHere.
Print SeeHere.
(* Module SeeHere := Struct Definition b : Set.
Definition a : b -> b.
End *)
My question is, this behaviour seems a bit random to me -- at least I don't find similar behaviour in OCaml's include -- what is the intention/main usage for this feature?
