New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))

 "Module M (...) := M1 <+ M2 <+ M3 <+ ..." is now a shortcut for
 "Module M (...). Include M1. Include M2. Include M3... End M."

 Moreover M2,M3,etc can be functors as long as they find what they need in what
 comes before them (see new command "Include Self").
 The only real constraint is that M1,M2,M3,... should not have common elements
 (for the moment (?)).

 Same behavior for signature : Module Type M := M1 <+ M2 <+ M3.

 Note that this <+ is _not_ a primitive construct of the module language,
 for instance it cannot be used in signature (Module M <: M1 <+ M2 is
 illegal for the moment).

 Some example of use in Decidable2 and NZAxioms

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12530 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions