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

2 files changed, 8 insertions, 8 deletions

diff --git a/theories/QArith/QOrderedType.v b/theories/QArith/QOrderedType.v
index cad77b4eb7..c49ded7403 100644
--- a/theories/QArith/QOrderedType.v
+++ b/theories/QArith/QOrderedType.v
@@ -20,8 +20,8 @@ Module Q_as_DT <: DecidableTypeFull.
  Definition eqb := Qeq_bool.
  Definition eqb_eq := Qeq_bool_iff.
 
- Include Self Backport_ET_fun. (** eq_refl, eq_sym, eq_trans *)
- Include Self Bool2Dec_fun. (** eq_dec *)
+ Include Backport_ET_fun. (** eq_refl, eq_sym, eq_trans *)
+ Include Bool2Dec_fun. (** eq_dec *)
 
 End Q_as_DT.
 
diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v
index afc5b9122e..087a6a7ddf 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.