The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Thu, 14 Jun 2012 10:21:30 -0300,
"Patricia Peratto" 
<psperatto AT adinet.com.uy>
 a écrit :

> What means the operator <+ by example in
> 
> Module Type EqLt := Typ <+ HasEq <+ HasLt.
> 
> (Library Orders.)
> 
> Patricia

See section 2.5.1 of coq reference manual:

It merges all the modules into one.

Module A.
  Definition t := true.
End A.

Module B.
  Definition f := false.
End B.

Module C.
  Definition t := false.
End C.

Module Ex2 := A <+ B.
Print Ex2.

Module Ex1 := A <+ B <+ C. (* does not work*)