No more specific syntax "Include Self" for inclusion of partially-applied functors

 For Module F(X:SIG), making now a Include F will try to find the X fields in
 the current context, just as was doing earlier Include Self F. This specific
 syntax is removed, freeing the keyword "Self". Anyway, with the use of the
 syntax "<+" there was already hardly any need for syntax "Include Self".
 Idem for Include Type.

 Beware that a typo such as "Include F" instead of "Include F G" will
 produce a different message now, about a missing field instead of
 a not-enough-applied functor.

 By the way, some code clean-up and factorisation of inner recursive
 functions in declaremods.ml.

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

1 files changed, 6 insertions, 6 deletions

diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v
index afc5b9122..087a6a7dd 100644
--- a/theories/Structures/DecidableType2.v
+++ b/theories/Structures/DecidableType2.v
@@ -99,16 +99,16 @@ Module UpdateEq (E:BareEquality)(F:IsEqOrig E) <: IsEq E.
 End UpdateEq.
 
 Module Backport_ET (E:EqualityType) <: EqualityTypeBoth
- := E <+ BackportEq E E.
+ := E <+ BackportEq.
 
 Module Update_ET (E:EqualityTypeOrig) <: EqualityTypeBoth
- := E <+ UpdateEq E E.
+ := E <+ UpdateEq.
 
 Module Backport_DT (E:DecidableType) <: DecidableTypeBoth
- := E <+ BackportEq E E.
+ := E <+ BackportEq.
 
 Module Update_DT (E:DecidableTypeOrig) <: DecidableTypeBoth
- := E <+ UpdateEq E E.
+ := E <+ UpdateEq.
 
 
 (** * Having [eq_dec] is equivalent to having [eqb] and its spec. *)
@@ -134,10 +134,10 @@ Module HasEqBool2Dec (E:BareEquality)(F:HasEqBool E) <: HasEqDec E.
 End HasEqBool2Dec.
 
 Module Dec2Bool (E:DecidableType) <: BooleanDecidableType
- := E <+ HasEqDec2Bool E E.
+ := E <+ HasEqDec2Bool.
 
 Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType
- := E <+ HasEqBool2Dec E E.
+ := E <+ HasEqBool2Dec.