aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/MSets/MSetInterface.v40
-rw-r--r--theories/Numbers/Integer/Abstract/ZAxioms.v2
-rw-r--r--theories/Numbers/Integer/Abstract/ZDivEucl.v4
-rw-r--r--theories/Numbers/Integer/Abstract/ZDivFloor.v4
-rw-r--r--theories/Numbers/Integer/Abstract/ZDivTrunc.v4
-rw-r--r--theories/Numbers/NatInt/NZAxioms.v12
-rw-r--r--theories/Numbers/NatInt/NZDiv.v4
-rw-r--r--theories/Numbers/Natural/Abstract/NAxioms.v2
-rw-r--r--theories/Numbers/Natural/Abstract/NDiv.v4
-rw-r--r--theories/Structures/DecidableType2.v2
-rw-r--r--theories/Structures/OrderTac.v6
-rw-r--r--theories/Structures/OrderedType2.v8
12 files changed, 46 insertions, 46 deletions
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index ec432de83..fbaa01c90 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -128,7 +128,7 @@ Module Type WSetsOn (E : DecidableType).
(** Logical predicates *)
Parameter In : elt -> t -> Prop.
- Instance In_compat : Proper (E.eq==>eq==>iff) In.
+ Declare Instance In_compat : Proper (E.eq==>eq==>iff) In.
Definition Equal s s' := forall a : elt, In a s <-> In a s'.
Definition Subset s s' := forall a : elt, In a s -> In a s'.
@@ -140,7 +140,7 @@ Module Type WSetsOn (E : DecidableType).
Notation "s [<=] t" := (Subset s t) (at level 70, no associativity).
Definition eq : t -> t -> Prop := Equal.
- Instance eq_equiv : Equivalence eq. (* obvious, for subtyping only *)
+ Declare Instance eq_equiv : Equivalence eq. (* obvious, for subtyping only *)
Parameter eq_dec : forall s s', { eq s s' } + { ~ eq s s' }.
(** Specifications of set operators *)
@@ -220,8 +220,8 @@ Module Type SetsOn (E : OrderedType).
Parameter lt : t -> t -> Prop.
(** Specification of [lt] *)
- Instance lt_strorder : StrictOrder lt.
- Instance lt_compat : Proper (eq==>eq==>iff) lt.
+ Declare Instance lt_strorder : StrictOrder lt.
+ Declare Instance lt_compat : Proper (eq==>eq==>iff) lt.
Section Spec.
Variable s s': t.
@@ -342,11 +342,11 @@ Module Type WRawSets (E : DecidableType).
predicate [Ok]. If [Ok] isn't decidable, [isok] may be the
always-false function. *)
Parameter isok : t -> bool.
- Instance isok_Ok s `(isok s = true) : Ok s | 10.
+ Declare Instance isok_Ok s `(isok s = true) : Ok s | 10.
(** Logical predicates *)
Parameter In : elt -> t -> Prop.
- Instance In_compat : Proper (E.eq==>eq==>iff) In.
+ Declare Instance In_compat : Proper (E.eq==>eq==>iff) In.
Definition Equal s s' := forall a : elt, In a s <-> In a s'.
Definition Subset s s' := forall a : elt, In a s -> In a s'.
@@ -358,20 +358,20 @@ Module Type WRawSets (E : DecidableType).
Notation "s [<=] t" := (Subset s t) (at level 70, no associativity).
Definition eq : t -> t -> Prop := Equal.
- Instance eq_equiv : Equivalence eq.
+ Declare Instance eq_equiv : Equivalence eq.
(** First, all operations are compatible with the well-formed predicate. *)
- Instance empty_ok : Ok empty.
- Instance add_ok s x `(Ok s) : Ok (add x s).
- Instance remove_ok s x `(Ok s) : Ok (remove x s).
- Instance singleton_ok x : Ok (singleton x).
- Instance union_ok s s' `(Ok s, Ok s') : Ok (union s s').
- Instance inter_ok s s' `(Ok s, Ok s') : Ok (inter s s').
- Instance diff_ok s s' `(Ok s, Ok s') : Ok (diff s s').
- Instance filter_ok s f `(Ok s) : Ok (filter f s).
- Instance partition_ok1 s f `(Ok s) : Ok (fst (partition f s)).
- Instance partition_ok2 s f `(Ok s) : Ok (snd (partition f s)).
+ Declare Instance empty_ok : Ok empty.
+ Declare Instance add_ok s x `(Ok s) : Ok (add x s).
+ Declare Instance remove_ok s x `(Ok s) : Ok (remove x s).
+ Declare Instance singleton_ok x : Ok (singleton x).
+ Declare Instance union_ok s s' `(Ok s, Ok s') : Ok (union s s').
+ Declare Instance inter_ok s s' `(Ok s, Ok s') : Ok (inter s s').
+ Declare Instance diff_ok s s' `(Ok s, Ok s') : Ok (diff s s').
+ Declare Instance filter_ok s f `(Ok s) : Ok (filter f s).
+ Declare Instance partition_ok1 s f `(Ok s) : Ok (fst (partition f s)).
+ Declare Instance partition_ok2 s f `(Ok s) : Ok (snd (partition f s)).
(** Now, the specifications, with constraints on the input sets. *)
@@ -562,8 +562,8 @@ Module Type RawSets (E : OrderedType).
Parameter lt : t -> t -> Prop.
(** Specification of [lt] *)
- Instance lt_strorder : StrictOrder lt.
- Instance lt_compat : Proper (eq==>eq==>iff) lt.
+ Declare Instance lt_strorder : StrictOrder lt.
+ Declare Instance lt_compat : Proper (eq==>eq==>iff) lt.
Section Spec.
Variable s s': t.
@@ -674,7 +674,7 @@ End Raw2Sets.
Module Type IN (O:OrderedType).
Parameter Inline t : Type.
Parameter Inline In : O.t -> t -> Prop.
- Instance In_compat : Proper (O.eq==>eq==>iff) In.
+ Declare Instance In_compat : Proper (O.eq==>eq==>iff) In.
Definition Equal s s' := forall x, In x s <-> In x s'.
Definition Empty s := forall x, ~In x s.
End IN.
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 4acb45401..4b3d18be4 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -19,7 +19,7 @@ Include Type NZOrdAxiomsSig.
Local Open Scope NumScope.
Parameter Inline opp : t -> t.
-Instance opp_wd : Proper (eq==>eq) opp.
+Declare Instance opp_wd : Proper (eq==>eq) opp.
Notation "- x" := (opp x) (at level 35, right associativity) : NumScope.
Notation "- 1" := (- (1)) : NumScope.
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index 0f15e9a29..2ec1cc9b0 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -33,8 +33,8 @@ Module Type ZDiv (Import Z : ZAxiomsSig).
Infix "/" := div : NumScope.
Infix "mod" := modulo (at level 40, no associativity) : NumScope.
- Instance div_wd : Proper (eq==>eq==>eq) div.
- Instance mod_wd : Proper (eq==>eq==>eq) modulo.
+ Declare Instance div_wd : Proper (eq==>eq==>eq) div.
+ Declare Instance mod_wd : Proper (eq==>eq==>eq) modulo.
Definition abs z := max z (-z).
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index b4a8a4203..473631293 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -36,8 +36,8 @@ Module Type ZDiv (Import Z : ZAxiomsSig).
Infix "/" := div : NumScope.
Infix "mod" := modulo (at level 40, no associativity) : NumScope.
- Instance div_wd : Proper (eq==>eq==>eq) div.
- Instance mod_wd : Proper (eq==>eq==>eq) modulo.
+ Declare Instance div_wd : Proper (eq==>eq==>eq) div.
+ Declare Instance mod_wd : Proper (eq==>eq==>eq) modulo.
Axiom div_mod : forall a b, b ~= 0 -> a == b*(a/b) + (a mod b).
Axiom mod_pos_bound : forall a b, 0 < b -> 0 <= a mod b < b.
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index fe2b262f2..2522f70c1 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -36,8 +36,8 @@ Module Type ZDiv (Import Z : ZAxiomsSig).
Infix "/" := div : NumScope.
Infix "mod" := modulo (at level 40, no associativity) : NumScope.
- Instance div_wd : Proper (eq==>eq==>eq) div.
- Instance mod_wd : Proper (eq==>eq==>eq) modulo.
+ Declare Instance div_wd : Proper (eq==>eq==>eq) div.
+ Declare Instance mod_wd : Proper (eq==>eq==>eq) modulo.
Axiom div_mod : forall a b, b ~= 0 -> a == b*(a/b) + (a mod b).
Axiom mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index ff220e793..f6328e249 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -37,8 +37,8 @@ Notation S := succ.
Notation P := pred.
Notation "1" := (S 0) : NumScope.
-Instance succ_wd : Proper (eq ==> eq) S.
-Instance pred_wd : Proper (eq ==> eq) P.
+Declare Instance succ_wd : Proper (eq ==> eq) S.
+Declare Instance pred_wd : Proper (eq ==> eq) P.
Axiom pred_succ : forall n, P (S n) == n.
@@ -67,9 +67,9 @@ Notation "x + y" := (add x y) : NumScope.
Notation "x - y" := (sub x y) : NumScope.
Notation "x * y" := (mul x y) : NumScope.
-Instance add_wd : Proper (eq ==> eq ==> eq) add.
-Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
-Instance mul_wd : Proper (eq ==> eq ==> eq) mul.
+Declare Instance add_wd : Proper (eq ==> eq ==> eq) add.
+Declare Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
+Declare Instance mul_wd : Proper (eq ==> eq ==> eq) mul.
Axiom add_0_l : forall n, (0 + n) == n.
Axiom add_succ_l : forall n m, (S n) + m == S (n + m).
@@ -107,7 +107,7 @@ Notation "x <= y <= z" := (x<=y /\ y<=z) : NumScope.
Notation "x <= y < z" := (x<=y /\ y<z) : NumScope.
Notation "x < y <= z" := (x<y /\ y<=z) : NumScope.
-Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
+Declare Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
(** Compatibility of [le] can be proved later from [lt_wd]
and [lt_eq_cases] *)
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index 62eee289d..1be2f8508 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -20,8 +20,8 @@ Module Type NZDiv (Import NZ : NZOrdAxiomsSig).
Infix "/" := div : NumScope.
Infix "mod" := modulo (at level 40, no associativity) : NumScope.
- Instance div_wd : Proper (eq==>eq==>eq) div.
- Instance mod_wd : Proper (eq==>eq==>eq) modulo.
+ Declare Instance div_wd : Proper (eq==>eq==>eq) div.
+ Declare Instance mod_wd : Proper (eq==>eq==>eq) modulo.
Axiom div_mod : forall a b, b ~= 0 -> a == b*(a/b) + (a mod b).
Axiom mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index bdabb1086..1cb474674 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -23,7 +23,7 @@ Axiom pred_0 : P 0 == 0.
Parameter Inline recursion : forall A : Type, A -> (t -> A -> A) -> t -> A.
Implicit Arguments recursion [A].
-Instance recursion_wd (A : Type) (Aeq : relation A) :
+Declare Instance recursion_wd (A : Type) (Aeq : relation A) :
Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A).
Axiom recursion_0 :
diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v
index 9ff9c08cf..1aa10958f 100644
--- a/theories/Numbers/Natural/Abstract/NDiv.v
+++ b/theories/Numbers/Natural/Abstract/NDiv.v
@@ -20,8 +20,8 @@ Module Type NDiv (Import N : NAxiomsSig).
Infix "/" := div : NumScope.
Infix "mod" := modulo (at level 40, no associativity) : NumScope.
- Instance div_wd : Proper (eq==>eq==>eq) div.
- Instance mod_wd : Proper (eq==>eq==>eq) modulo.
+ Declare Instance div_wd : Proper (eq==>eq==>eq) div.
+ Declare Instance mod_wd : Proper (eq==>eq==>eq) modulo.
Axiom div_mod : forall a b, b ~= 0 -> a == b*(a/b) + (a mod b).
Axiom mod_upper_bound : forall a b, b ~= 0 -> a mod b < b.
diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v
index 087a6a7dd..0957ef243 100644
--- a/theories/Structures/DecidableType2.v
+++ b/theories/Structures/DecidableType2.v
@@ -23,7 +23,7 @@ End BareEquality.
(** * Specification of the equality by the Type Classe [Equivalence] *)
Module Type IsEq (Import E:BareEquality).
- Instance eq_equiv : Equivalence eq.
+ Declare Instance eq_equiv : Equivalence eq.
Hint Resolve (@Equivalence_Reflexive _ _ eq_equiv).
Hint Resolve (@Equivalence_Transitive _ _ eq_equiv).
Hint Immediate (@Equivalence_Symmetric _ _ eq_equiv).
diff --git a/theories/Structures/OrderTac.v b/theories/Structures/OrderTac.v
index 8a3635686..f75e1ae91 100644
--- a/theories/Structures/OrderTac.v
+++ b/theories/Structures/OrderTac.v
@@ -31,9 +31,9 @@ Module Type OrderSig.
Parameter Inline t : Type.
Parameters eq lt le : t -> t -> Prop.
-Instance eq_equiv : Equivalence eq.
-Instance lt_strorder : StrictOrder lt.
-Instance lt_compat : Proper (eq==>eq==>iff) lt.
+Declare Instance eq_equiv : Equivalence eq.
+Declare Instance lt_strorder : StrictOrder lt.
+Declare Instance lt_compat : Proper (eq==>eq==>iff) lt.
Parameter lt_total : forall x y, lt x y \/ eq x y \/ lt y x.
Parameter le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v
index 310f99a4a..be7ec153b 100644
--- a/theories/Structures/OrderedType2.v
+++ b/theories/Structures/OrderedType2.v
@@ -18,8 +18,8 @@ Module Type MiniOrderedType.
Include Type EqualityType.
Parameter Inline lt : t -> t -> Prop.
- Instance lt_strorder : StrictOrder lt.
- Instance lt_compat : Proper (eq==>eq==>iff) lt.
+ Declare Instance lt_strorder : StrictOrder lt.
+ Declare Instance lt_compat : Proper (eq==>eq==>iff) lt.
Parameter Inline compare : t -> t -> comparison.
Axiom compare_spec : forall x y, CompSpec eq lt x y (compare x y).
@@ -63,10 +63,10 @@ Module Type UsualOrderedType.
Include Type UsualDecidableType.
Parameter Inline lt : t -> t -> Prop.
- Instance lt_strorder : StrictOrder lt.
+ Declare Instance lt_strorder : StrictOrder lt.
(* The following is useless since eq is Leibniz, but should be there
for subtyping... *)
- Instance lt_compat : Proper (eq==>eq==>iff) lt.
+ Declare Instance lt_compat : Proper (eq==>eq==>iff) lt.
Parameter Inline compare : t -> t -> comparison.
Axiom compare_spec : forall x y, CompSpec eq lt x y (compare x y).
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 03:57:18 +0000