aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/FSets/FMapInterface.v6
-rw-r--r--theories/FSets/FSetInterface.v6
-rw-r--r--theories/MSets/MSetInterface.v18
-rw-r--r--theories/Numbers/Integer/Abstract/ZBase.v2
-rw-r--r--theories/Numbers/Integer/Abstract/ZProperties.v2
-rw-r--r--theories/Numbers/NatInt/NZAddOrder.v2
-rw-r--r--theories/Numbers/NatInt/NZMul.v2
-rw-r--r--theories/Numbers/NatInt/NZMulOrder.v2
-rw-r--r--theories/Numbers/NatInt/NZOrder.v5
-rw-r--r--theories/Numbers/Natural/Abstract/NBase.v2
-rw-r--r--theories/Numbers/Natural/Abstract/NProperties.v2
-rw-r--r--theories/Numbers/Natural/Abstract/NStrongRec.v2
-rw-r--r--theories/Structures/OrderTac.v4
-rw-r--r--theories/Structures/OrderedType.v2
-rw-r--r--theories/Structures/OrderedType2.v2
15 files changed, 29 insertions, 30 deletions
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index cd51b2aff..e60cca9d9 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -258,7 +258,7 @@ End WSfun.
Module Type WS.
Declare Module E : DecidableType.
- Include Type WSfun E.
+ Include WSfun E.
End WS.
@@ -266,7 +266,7 @@ End WS.
(** ** Maps on ordered keys, functorial signature *)
Module Type Sfun (E : OrderedType).
- Include Type WSfun E.
+ Include WSfun E.
Section elt.
Variable elt:Type.
Definition lt_key (p p':key*elt) := E.lt (fst p) (fst p').
@@ -284,7 +284,7 @@ End Sfun.
Module Type S.
Declare Module E : OrderedType.
- Include Type Sfun E.
+ Include Sfun E.
End S.
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index d94ff7c95..8aede5527 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -275,7 +275,7 @@ End WSfun.
Module Type WS.
Declare Module E : DecidableType.
- Include Type WSfun E.
+ Include WSfun E.
End WS.
@@ -286,7 +286,7 @@ End WS.
and some stronger specifications for other functions. *)
Module Type Sfun (E : OrderedType).
- Include Type WSfun E.
+ Include WSfun E.
Parameter lt : t -> t -> Prop.
Parameter compare : forall s s' : t, Compare lt eq s s'.
@@ -349,7 +349,7 @@ End Sfun.
Module Type S.
Declare Module E : OrderedType.
- Include Type Sfun E.
+ Include Sfun E.
End S.
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index effd5e35a..cb18785e6 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -117,7 +117,7 @@ End HasWOps.
Module Type WOps (E : DecidableType).
Definition elt := E.t.
Parameter t : Type. (** the abstract type of sets *)
- Include Type HasWOps.
+ Include HasWOps.
End WOps.
@@ -128,7 +128,7 @@ End WOps.
Module Type WSetsOn (E : DecidableType).
(** First, we ask for all the functions *)
- Include Type WOps E.
+ Include WOps E.
(** Logical predicates *)
Parameter In : elt -> t -> Prop.
@@ -144,8 +144,8 @@ Module Type WSetsOn (E : DecidableType).
Notation "s [<=] t" := (Subset s t) (at level 70, no associativity).
Definition eq : t -> t -> Prop := Equal.
- Include Type IsEq. (** [eq] is obviously an equivalence, for subtyping only *)
- Include Type HasEqDec.
+ Include IsEq. (** [eq] is obviously an equivalence, for subtyping only *)
+ Include HasEqDec.
(** Specifications of set operators *)
@@ -197,7 +197,7 @@ End WSetsOn.
Module Type WSets.
Declare Module E : DecidableType.
- Include Type WSetsOn E.
+ Include WSetsOn E.
End WSets.
(** ** Functorial signature for sets on ordered elements
@@ -226,7 +226,7 @@ Module Type Ops (E : OrderedType) := WOps E <+ HasOrdOps.
Module Type SetsOn (E : OrderedType).
- Include Type WSetsOn E <+ HasOrdOps <+ HasLt <+ IsStrOrder.
+ Include WSetsOn E <+ HasOrdOps <+ HasLt <+ IsStrOrder.
Section Spec.
Variable s s': t.
@@ -266,7 +266,7 @@ End SetsOn.
Module Type Sets.
Declare Module E : OrderedType.
- Include Type SetsOn E.
+ Include SetsOn E.
End Sets.
Module Type S := Sets.
@@ -335,7 +335,7 @@ Module WS_WSfun (M : WSets) <: WSetsOn M.E := M.
Module Type WRawSets (E : DecidableType).
(** First, we ask for all the functions *)
- Include Type WOps E.
+ Include WOps E.
(** Is a set well-formed or ill-formed ? *)
@@ -559,7 +559,7 @@ End WRaw2Sets.
(** Same approach for ordered sets *)
Module Type RawSets (E : OrderedType).
- Include Type WRawSets E <+ HasOrdOps <+ HasLt <+ IsStrOrder.
+ Include WRawSets E <+ HasOrdOps <+ HasLt <+ IsStrOrder.
Section Spec.
Variable s s': t.
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 9b5a80762..44bb02ecc 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -15,7 +15,7 @@ Require Export ZAxioms.
Require Import NZProperties.
Module ZBasePropFunct (Import Z : ZAxiomsSig').
-Include Type NZPropFunct Z.
+Include NZPropFunct Z.
(* Theorems that are true for integers but not for natural numbers *)
diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v
index 7f2253205..9b6f0ff64 100644
--- a/theories/Numbers/Integer/Abstract/ZProperties.v
+++ b/theories/Numbers/Integer/Abstract/ZProperties.v
@@ -18,6 +18,6 @@ Require Export ZAxioms ZMulOrder.
Module Type ZPropSig := ZMulOrderPropFunct.
Module ZPropFunct (Z:ZAxiomsSig) <: ZPropSig Z.
- Include Type ZPropSig Z.
+ Include ZPropSig Z.
End ZPropFunct.
diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index 7313c4131..97c122029 100644
--- a/theories/Numbers/NatInt/NZAddOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.v
@@ -13,7 +13,7 @@
Require Import NZAxioms NZBase NZMul NZOrder.
Module Type NZAddOrderPropSig (Import NZ : NZOrdAxiomsSig').
-Include Type NZBasePropSig NZ <+ NZMulPropSig NZ <+ NZOrderPropSig NZ.
+Include NZBasePropSig NZ <+ NZMulPropSig NZ <+ NZOrderPropSig NZ.
Theorem add_lt_mono_l : forall n m p, n < m <-> p + n < p + m.
Proof.
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v
index 3c11024e5..296bd095f 100644
--- a/theories/Numbers/NatInt/NZMul.v
+++ b/theories/Numbers/NatInt/NZMul.v
@@ -14,7 +14,7 @@ Require Import NZAxioms NZBase NZAdd.
Module Type NZMulPropSig
(Import NZ : NZAxiomsSig')(Import NZBase : NZBasePropSig NZ).
-Include Type NZAddPropSig NZ NZBase.
+Include NZAddPropSig NZ NZBase.
Theorem mul_0_r : forall n, n * 0 == 0.
Proof.
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index 18f61de59..7b64a6983 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -14,7 +14,7 @@ Require Import NZAxioms.
Require Import NZAddOrder.
Module Type NZMulOrderPropSig (Import NZ : NZOrdAxiomsSig').
-Include Type NZAddOrderPropSig NZ.
+Include NZAddOrderPropSig NZ.
Theorem mul_lt_pred :
forall p q n m, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 6697c0b3d..6a086f3bd 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -611,7 +611,6 @@ End WF.
End NZOrderPropSig.
-Module NZOrderPropFunct (Import NZ : NZOrdSig).
- Include Type NZBasePropSig NZ <+ NZOrderPropSig NZ.
-End NZOrderPropFunct.
+Module NZOrderPropFunct (NZ : NZOrdSig) :=
+ NZBasePropSig NZ <+ NZOrderPropSig NZ.
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 0d489a16d..842f4bcf2 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -16,7 +16,7 @@ Require Import NZProperties.
Module NBasePropFunct (Import N : NAxiomsSig').
(** First, we import all known facts about both natural numbers and integers. *)
-Include Type NZPropFunct N.
+Include NZPropFunct N.
(** We prove that the successor of a number is not zero by defining a
function (by recursion) that maps 0 to false and the successor to true *)
diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v
index 2baed54cf..30262bd9f 100644
--- a/theories/Numbers/Natural/Abstract/NProperties.v
+++ b/theories/Numbers/Natural/Abstract/NProperties.v
@@ -18,5 +18,5 @@ Require Export NAxioms NSub.
Module Type NPropSig := NSubPropFunct.
Module NPropFunct (N:NAxiomsSig) <: NPropSig N.
- Include Type NPropSig N.
+ Include NPropSig N.
End NPropFunct.
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index ed867b825..cbbcdbff5 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -16,7 +16,7 @@ and proves its properties *)
Require Export NSub.
Module NStrongRecPropFunct (Import N : NAxiomsSig').
-Include Type NSubPropFunct N.
+Include NSubPropFunct N.
Section StrongRecursion.
diff --git a/theories/Structures/OrderTac.v b/theories/Structures/OrderTac.v
index 43df377c0..2465dc539 100644
--- a/theories/Structures/OrderTac.v
+++ b/theories/Structures/OrderTac.v
@@ -53,7 +53,7 @@ Local Infix "+" := trans_ord.
Module Type TotalOrder_NoInline <: TotalOrder.
Parameter Inline t : Type.
Parameters eq lt le : t -> t -> Prop.
- Include Type IsEq <+ IsStrOrder <+ LeIsLtEq <+ LtIsTotal.
+ Include IsEq <+ IsStrOrder <+ LeIsLtEq <+ LtIsTotal.
End TotalOrder_NoInline.
Module Type TotalOrder_NoInline' := TotalOrder_NoInline <+ EqLtLeNotation.
@@ -302,7 +302,7 @@ Definition t := O.t.
Definition eq := O.eq.
Definition lt := flip O.lt.
Definition le := flip O.le.
-Include Type EqLtLeNotation.
+Include EqLtLeNotation.
Instance eq_equiv : Equivalence eq.
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index ca441fc86..1f3e50dc3 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -41,7 +41,7 @@ Module Type MiniOrderedType.
End MiniOrderedType.
Module Type OrderedType.
- Include Type MiniOrderedType.
+ Include MiniOrderedType.
(** A [eq_dec] can be deduced from [compare] below. But adding this
redundant field allows to see an OrderedType as a DecidableType. *)
diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v
index 1cddfea3b..766b0faf0 100644
--- a/theories/Structures/OrderedType2.v
+++ b/theories/Structures/OrderedType2.v
@@ -43,7 +43,7 @@ Module Type LeNotation (E:EqLe).
End LeNotation.
Module Type LtLeNotation (E:EqLtLe).
- Include Type LtNotation E <+ LeNotation E.
+ Include LtNotation E <+ LeNotation E.
Notation "x <= y < z" := (x<=y /\ y<z).
Notation "x < y <= z" := (x<y /\ y<=z).
End LtLeNotation.
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 17:19:59 +0000