The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

It's a shorthand for taking a module, opening it, and "extending" it
by including other modules:
http://coq.inria.fr/doc/Reference-Manual004.html

From section 2.5.3:
> Module ident module_bindings := module_expression1 <+ … <+ 
> module_expressionn
> is equivalent to an interactive module where each module_expressioni are 
> included.

Kris


On Mon, Sep 23, 2013 at 6:06 PM, Patricia Peratto
<psperatto AT adinet.com.uy>
 wrote:
> Which is the meaning of the operator <+
> in Module Types, by example in
>
> Module Type EqLt := Typ <+ HasEq <+ HasLt.
>
> in module Orders?
>
> Patricia