From 35159e8aa9bf33b4882bc7f17c2e363f769624c7 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 7 Dec 2009 15:24:13 +0000
Subject: 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
---
 theories/Structures/DecidableType2.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'theories/Structures')

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.
 
 
 
-- 
cgit v1.2.3