aboutsummaryrefslogtreecommitdiff
path: root/theories/Classes
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Classes')
-rw-r--r--theories/Classes/CMorphisms.v41
-rw-r--r--theories/Classes/CRelationClasses.v15
-rw-r--r--theories/Classes/Init.v1
-rw-r--r--theories/Classes/Morphisms.v36
-rw-r--r--theories/Classes/Morphisms_Relations.v8
-rw-r--r--theories/Classes/RelationClasses.v21
-rw-r--r--theories/Classes/RelationPairs.v16
7 files changed, 104 insertions, 34 deletions
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 9a3a1d3709..9ff18ebe2c 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -1,4 +1,4 @@
-(* -*- coding: utf-8; coq-prog-args: ("-coqlib" "../.." "-R" ".." "Coq" "-top" "Coq.Classes.CMorphisms") -*- *)
+(* -*- coding: utf-8; coq-prog-args: ("-top" "Coq.Classes.CMorphisms") -*- *)
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
@@ -80,9 +80,11 @@ End Proper.
(** We favor the use of Leibniz equality or a declared reflexive crelation
when resolving [ProperProxy], otherwise, if the crelation is given (not an evar),
we fall back to [Proper]. *)
+#[global]
Hint Extern 1 (ProperProxy _ _) =>
class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances.
+#[global]
Hint Extern 2 (ProperProxy ?R _) =>
not_evar R; class_apply @proper_proper_proxy : typeclass_instances.
@@ -215,8 +217,11 @@ Typeclasses Opaque respectful pointwise_relation forall_relation.
Arguments forall_relation {A P}%type sig%signature _ _.
Arguments pointwise_relation A%type {B}%type R%signature _ _.
+#[global]
Hint Unfold Reflexive : core.
+#[global]
Hint Unfold Symmetric : core.
+#[global]
Hint Unfold Transitive : core.
(** Resolution with subrelation: favor decomposing products over applying reflexivity
@@ -225,6 +230,7 @@ Ltac subrelation_tac T U :=
(is_ground T ; is_ground U ; class_apply @subrelation_refl) ||
class_apply @subrelation_respectful || class_apply @subrelation_refl.
+#[global]
Hint Extern 3 (@subrelation _ ?T ?U) => subrelation_tac T U : typeclass_instances.
CoInductive apply_subrelation : Prop := do_subrelation.
@@ -234,6 +240,7 @@ Ltac proper_subrelation :=
[ H : apply_subrelation |- _ ] => clear H ; class_apply @subrelation_proper
end.
+#[global]
Hint Extern 5 (@Proper _ ?H _) => proper_subrelation : typeclass_instances.
(** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
@@ -254,6 +261,7 @@ Proof. firstorder. Qed.
(** We use an extern hint to help unification. *)
+#[global]
Hint Extern 4 (subrelation (@forall_relation ?A ?B ?R) (@forall_relation _ _ ?S)) =>
apply (@forall_subrelation A B R S) ; intro : typeclass_instances.
@@ -308,7 +316,7 @@ Section GenericInstances.
Global Program
Instance trans_contra_inv_impl_type_morphism
- `(Transitive A R) : Proper (R --> flip arrow) (R x) | 3.
+ `(Transitive A R) {x} : Proper (R --> flip arrow) (R x) | 3.
Next Obligation.
Proof with auto.
@@ -318,7 +326,7 @@ Section GenericInstances.
Global Program
Instance trans_co_impl_type_morphism
- `(Transitive A R) : Proper (R ++> arrow) (R x) | 3.
+ `(Transitive A R) {x} : Proper (R ++> arrow) (R x) | 3.
Next Obligation.
Proof with auto.
@@ -328,7 +336,7 @@ Section GenericInstances.
Global Program
Instance trans_sym_co_inv_impl_type_morphism
- `(PER A R) : Proper (R ++> flip arrow) (R x) | 3.
+ `(PER A R) {x} : Proper (R ++> flip arrow) (R x) | 3.
Next Obligation.
Proof with auto.
@@ -337,7 +345,7 @@ Section GenericInstances.
Qed.
Global Program Instance trans_sym_contra_arrow_morphism
- `(PER A R) : Proper (R --> arrow) (R x) | 3.
+ `(PER A R) {x} : Proper (R --> arrow) (R x) | 3.
Next Obligation.
Proof with auto.
@@ -346,7 +354,7 @@ Section GenericInstances.
Qed.
Global Program Instance per_partial_app_type_morphism
- `(PER A R) : Proper (R ==> iffT) (R x) | 2.
+ `(PER A R) {x} : Proper (R ==> iffT) (R x) | 2.
Next Obligation.
Proof with auto.
@@ -399,17 +407,17 @@ Section GenericInstances.
(** Coq functions are morphisms for Leibniz equality,
applied only if really needed. *)
- Global Instance reflexive_eq_dom_reflexive `(Reflexive B R') :
+ Global Instance reflexive_eq_dom_reflexive `(Reflexive B R') {A} :
Reflexive (@Logic.eq A ==> R').
Proof. simpl_crelation. Qed.
(** [respectful] is a morphism for crelation equivalence . *)
- Global Instance respectful_morphism :
+ Global Instance respectful_morphism {A B} :
Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence)
(@respectful A B).
Proof.
- intros A B R R' HRR' S S' HSS' f g.
+ intros R R' HRR' S S' HSS' f g.
unfold respectful , relation_equivalence in *; simpl in *.
split ; intros H x y Hxy.
- apply (fst (HSS' _ _)). apply H. now apply (snd (HRR' _ _)).
@@ -511,9 +519,9 @@ Ltac partial_application_tactic :=
(** Bootstrap !!! *)
-Instance proper_proper : Proper (relation_equivalence ==> eq ==> iffT) (@Proper A).
+Instance proper_proper {A} : Proper (relation_equivalence ==> eq ==> iffT) (@Proper A).
Proof.
- intros A R R' HRR' x y <-. red in HRR'.
+ intros R R' HRR' x y <-. red in HRR'.
split ; red ; intros.
- now apply (fst (HRR' _ _)).
- now apply (snd (HRR' _ _)).
@@ -526,17 +534,23 @@ Ltac proper_reflexive :=
end.
+#[global]
Hint Extern 1 (subrelation (flip _) _) => class_apply @flip1 : typeclass_instances.
+#[global]
Hint Extern 1 (subrelation _ (flip _)) => class_apply @flip2 : typeclass_instances.
(* Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper *)
(* : typeclass_instances. *)
+#[global]
Hint Extern 1 (Proper _ (flip _)) => apply @flip_proper
: typeclass_instances.
+#[global]
Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_flip_proper
: typeclass_instances.
+#[global]
Hint Extern 4 (@Proper _ _ _) => partial_application_tactic
: typeclass_instances.
+#[global]
Hint Extern 7 (@Proper _ _ _) => proper_reflexive
: typeclass_instances.
@@ -586,7 +600,9 @@ Ltac proper_normalization :=
set(H:=did_normalization) ; class_apply @proper_normalizes_proper
end.
+#[global]
Hint Extern 1 (Normalizes _ _ _) => normalizes : typeclass_instances.
+#[global]
Hint Extern 6 (@Proper _ _ _) => proper_normalization
: typeclass_instances.
@@ -690,6 +706,7 @@ split.
+ right. transitivity y; auto.
Qed.
+#[global]
Hint Extern 4 (PreOrder (relation_disjunction _ _)) =>
class_apply StrictOrder_PreOrder : typeclass_instances.
@@ -702,8 +719,10 @@ elim (StrictOrder_Irreflexive x).
transitivity y; auto.
Qed.
+#[global]
Hint Extern 4 (StrictOrder (relation_conjunction _ _)) =>
class_apply PartialOrder_StrictOrder : typeclass_instances.
+#[global]
Hint Extern 4 (PartialOrder _ (relation_disjunction _ _)) =>
class_apply StrictOrder_PartialOrder : typeclass_instances.
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v
index 72a196ca7a..236d35b68e 100644
--- a/theories/Classes/CRelationClasses.v
+++ b/theories/Classes/CRelationClasses.v
@@ -203,22 +203,35 @@ Defined.
(** Hints to drive the typeclass resolution avoiding loops
due to the use of full unification. *)
+#[global]
Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances.
+#[global]
Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances.
+#[global]
Hint Extern 3 (Irreflexive (complement _)) => class_apply complement_Irreflexive : typeclass_instances.
+#[global]
Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances.
+#[global]
Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances.
+#[global]
Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances.
+#[global]
Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances.
+#[global]
Hint Extern 3 (Antisymmetric (flip _)) => class_apply flip_Antisymmetric : typeclass_instances.
+#[global]
Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances.
+#[global]
Hint Extern 3 (StrictOrder (flip _)) => class_apply flip_StrictOrder : typeclass_instances.
+#[global]
Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_instances.
+#[global]
Hint Extern 4 (subrelation (flip _) _) =>
class_apply @subrelation_symmetric : typeclass_instances.
+#[global]
Hint Resolve irreflexivity : ord.
Unset Implicit Arguments.
@@ -231,6 +244,7 @@ Ltac solve_crelation :=
| [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H
end.
+#[global]
Hint Extern 4 => solve_crelation : crelations.
(** We can already dualize all these properties. *)
@@ -351,6 +365,7 @@ Section Binary.
Qed.
End Binary.
+#[global]
Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances.
(** The partial order defined by subrelation and crelation equivalence. *)
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 394f5dc4de..9ca465bbfd 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -36,4 +36,5 @@ Ltac unconvertible :=
| |- _ => exact tt
end.
+#[global]
Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index c70e3fe478..87abc4a08f 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,4 +1,4 @@
-(* -*- coding: utf-8; coq-prog-args: ("-coqlib" "../.." "-R" ".." "Coq" "-top" "Coq.Classes.Morphisms") -*- *)
+(* -*- coding: utf-8; coq-prog-args: ("-top" "Coq.Classes.Morphisms") -*- *)
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
@@ -81,9 +81,11 @@ End Proper.
(** We favor the use of Leibniz equality or a declared reflexive relation
when resolving [ProperProxy], otherwise, if the relation is given (not an evar),
we fall back to [Proper]. *)
+#[global]
Hint Extern 1 (ProperProxy _ _) =>
class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances.
+#[global]
Hint Extern 2 (ProperProxy ?R _) =>
not_evar R; class_apply @proper_proper_proxy : typeclass_instances.
@@ -213,8 +215,11 @@ Typeclasses Opaque respectful pointwise_relation forall_relation.
Arguments forall_relation {A P}%type sig%signature _ _.
Arguments pointwise_relation A%type {B}%type R%signature _ _.
+#[global]
Hint Unfold Reflexive : core.
+#[global]
Hint Unfold Symmetric : core.
+#[global]
Hint Unfold Transitive : core.
(** Resolution with subrelation: favor decomposing products over applying reflexivity
@@ -223,6 +228,7 @@ Ltac subrelation_tac T U :=
(is_ground T ; is_ground U ; class_apply @subrelation_refl) ||
class_apply @subrelation_respectful || class_apply @subrelation_refl.
+#[global]
Hint Extern 3 (@subrelation _ ?T ?U) => subrelation_tac T U : typeclass_instances.
CoInductive apply_subrelation : Prop := do_subrelation.
@@ -232,6 +238,7 @@ Ltac proper_subrelation :=
[ H : apply_subrelation |- _ ] => clear H ; class_apply @subrelation_proper
end.
+#[global]
Hint Extern 5 (@Proper _ ?H _) => proper_subrelation : typeclass_instances.
(** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
@@ -244,6 +251,7 @@ Proof. firstorder. Qed.
(** We use an extern hint to help unification. *)
+#[global]
Hint Extern 4 (subrelation (@forall_relation ?A ?B ?R) (@forall_relation _ _ ?S)) =>
apply (@forall_subrelation A B R S) ; intro : typeclass_instances.
@@ -309,7 +317,7 @@ Section GenericInstances.
Global Program
Instance trans_contra_inv_impl_morphism
- `(Transitive A R) : Proper (R --> flip impl) (R x) | 3.
+ `(Transitive A R) {x} : Proper (R --> flip impl) (R x) | 3.
Next Obligation.
Proof with auto.
@@ -319,7 +327,7 @@ Section GenericInstances.
Global Program
Instance trans_co_impl_morphism
- `(Transitive A R) : Proper (R ++> impl) (R x) | 3.
+ `(Transitive A R) {x} : Proper (R ++> impl) (R x) | 3.
Next Obligation.
Proof with auto.
@@ -329,7 +337,7 @@ Section GenericInstances.
Global Program
Instance trans_sym_co_inv_impl_morphism
- `(PER A R) : Proper (R ++> flip impl) (R x) | 3.
+ `(PER A R) {x} : Proper (R ++> flip impl) (R x) | 3.
Next Obligation.
Proof with auto.
@@ -338,7 +346,7 @@ Section GenericInstances.
Qed.
Global Program Instance trans_sym_contra_impl_morphism
- `(PER A R) : Proper (R --> impl) (R x) | 3.
+ `(PER A R) {x} : Proper (R --> impl) (R x) | 3.
Next Obligation.
Proof with auto.
@@ -347,7 +355,7 @@ Section GenericInstances.
Qed.
Global Program Instance per_partial_app_morphism
- `(PER A R) : Proper (R ==> iff) (R x) | 2.
+ `(PER A R) {x} : Proper (R ==> iff) (R x) | 2.
Next Obligation.
Proof with auto.
@@ -520,9 +528,9 @@ Ltac partial_application_tactic :=
(** Bootstrap !!! *)
-Instance proper_proper : Proper (relation_equivalence ==> eq ==> iff) (@Proper A).
+Instance proper_proper {A} : Proper (relation_equivalence ==> eq ==> iff) (@Proper A).
Proof.
- intros A x y H y0 y1 e; destruct e.
+ intros x y H y0 y1 e; destruct e.
reduce in H.
split ; red ; intros H0.
- setoid_rewrite <- H.
@@ -538,17 +546,24 @@ Ltac proper_reflexive :=
end.
+#[global]
Hint Extern 1 (subrelation (flip _) _) => class_apply @flip1 : typeclass_instances.
+#[global]
Hint Extern 1 (subrelation _ (flip _)) => class_apply @flip2 : typeclass_instances.
+#[global]
Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper
: typeclass_instances.
+#[global]
Hint Extern 1 (Proper _ (flip _)) => apply @flip_proper
: typeclass_instances.
+#[global]
Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_flip_proper
: typeclass_instances.
+#[global]
Hint Extern 4 (@Proper _ _ _) => partial_application_tactic
: typeclass_instances.
+#[global]
Hint Extern 7 (@Proper _ _ _) => proper_reflexive
: typeclass_instances.
@@ -603,7 +618,9 @@ Ltac proper_normalization :=
set(H:=did_normalization) ; class_apply @proper_normalizes_proper
end.
+#[global]
Hint Extern 1 (Normalizes _ _ _) => normalizes : typeclass_instances.
+#[global]
Hint Extern 6 (@Proper _ _ _) => proper_normalization
: typeclass_instances.
@@ -693,6 +710,7 @@ split.
+ right. transitivity y; auto.
Qed.
+#[global]
Hint Extern 4 (PreOrder (relation_disjunction _ _)) =>
class_apply StrictOrder_PreOrder : typeclass_instances.
@@ -705,8 +723,10 @@ elim (StrictOrder_Irreflexive x).
transitivity y; auto.
Qed.
+#[global]
Hint Extern 4 (StrictOrder (relation_conjunction _ _)) =>
class_apply PartialOrder_StrictOrder : typeclass_instances.
+#[global]
Hint Extern 4 (PartialOrder _ (relation_disjunction _ _)) =>
class_apply StrictOrder_PartialOrder : typeclass_instances.
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index a168a8e7cd..964786d8e6 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -22,11 +22,11 @@ Generalizable Variables A l.
(** Morphisms for relations *)
-Instance relation_conjunction_morphism : Proper (relation_equivalence (A:=A) ==>
+Instance relation_conjunction_morphism {A} : Proper (relation_equivalence (A:=A) ==>
relation_equivalence ==> relation_equivalence) relation_conjunction.
Proof. firstorder. Qed.
-Instance relation_disjunction_morphism : Proper (relation_equivalence (A:=A) ==>
+Instance relation_disjunction_morphism {A} : Proper (relation_equivalence (A:=A) ==>
relation_equivalence ==> relation_equivalence) relation_disjunction.
Proof. firstorder. Qed.
@@ -43,11 +43,11 @@ Proof. do 2 red. unfold predicate_implication. auto. Qed.
(** The instantiation at relation allows rewriting applications of relations
[R x y] to [R' x y] when [R] and [R'] are in [relation_equivalence]. *)
-Instance relation_equivalence_pointwise :
+Instance relation_equivalence_pointwise {A} :
Proper (relation_equivalence ==> pointwise_relation A (pointwise_relation A iff)) id.
Proof. intro. apply (predicate_equivalence_pointwise (Tcons A (Tcons A Tnil))). Qed.
-Instance subrelation_pointwise :
+Instance subrelation_pointwise {A} :
Proper (subrelation ==> pointwise_relation A (pointwise_relation A impl)) id.
Proof. intro. apply (predicate_implication_pointwise (Tcons A (Tcons A Tnil))). Qed.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 5381e91997..54ee06343a 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -196,19 +196,31 @@ Defined.
(** Hints to drive the typeclass resolution avoiding loops
due to the use of full unification. *)
+#[global]
Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances.
+#[global]
Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances.
+#[global]
Hint Extern 3 (Irreflexive (complement _)) => class_apply complement_Irreflexive : typeclass_instances.
+#[global]
Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances.
+#[global]
Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances.
+#[global]
Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances.
+#[global]
Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances.
+#[global]
Hint Extern 3 (Antisymmetric (flip _)) => class_apply flip_Antisymmetric : typeclass_instances.
+#[global]
Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances.
+#[global]
Hint Extern 3 (StrictOrder (flip _)) => class_apply flip_StrictOrder : typeclass_instances.
+#[global]
Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_instances.
+#[global]
Hint Extern 4 (subrelation (flip _) _) =>
class_apply @subrelation_symmetric : typeclass_instances.
@@ -218,6 +230,7 @@ Arguments asymmetry {A} {R} {_} [x] [y] _ _.
Arguments transitivity {A} {R} {_} [x] [y] [z] _ _.
Arguments Antisymmetric A eqA {_} _.
+#[global]
Hint Resolve irreflexivity : ord.
Unset Implicit Arguments.
@@ -230,6 +243,7 @@ Ltac solve_relation :=
| [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H
end.
+#[global]
Hint Extern 4 => solve_relation : relations.
(** We can already dualize all these properties. *)
@@ -395,7 +409,7 @@ Notation "∙⊥∙" := false_predicate : predicate_scope.
(** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *)
-Program Instance predicate_equivalence_equivalence :
+Program Instance predicate_equivalence_equivalence {l} :
Equivalence (@predicate_equivalence l).
Next Obligation.
@@ -413,7 +427,7 @@ Program Instance predicate_equivalence_equivalence :
firstorder.
Qed.
-Program Instance predicate_implication_preorder :
+Program Instance predicate_implication_preorder {l} :
PreOrder (@predicate_implication l).
Next Obligation.
intro l; induction l ; firstorder.
@@ -476,11 +490,12 @@ Section Binary.
Proof. firstorder. Qed.
End Binary.
+#[global]
Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances.
(** The partial order defined by subrelation and relation equivalence. *)
-Program Instance subrelation_partial_order :
+Program Instance subrelation_partial_order {A} :
PartialOrder (@relation_equivalence A) subrelation.
Next Obligation.
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index b4034b9cf9..87e66a25dd 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -61,11 +61,9 @@ Class Measure {A B} (f : A -> B).
(** Standard measures. *)
-Instance fst_measure : @Measure (A * B) A Fst.
-Defined.
+Instance fst_measure {A B} : @Measure (A * B) A Fst := {}.
-Instance snd_measure : @Measure (A * B) B Snd.
-Defined.
+Instance snd_measure {A B} : @Measure (A * B) B Snd := {}.
(** We define a product relation over [A*B]: each components should
satisfy the corresponding initial relation. *)
@@ -96,11 +94,11 @@ Section RelCompFun_Instances.
`(Measure A B f, Irreflexive _ R) : Irreflexive (R@@f).
Proof. firstorder. Qed.
- Global Program Instance RelCompFun_Equivalence
- `(Measure A B f, Equivalence _ R) : Equivalence (R@@f).
+ Global Instance RelCompFun_Equivalence
+ `(Measure A B f, Equivalence _ R) : Equivalence (R@@f) := {}.
- Global Program Instance RelCompFun_StrictOrder
- `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f).
+ Global Instance RelCompFun_StrictOrder
+ `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f) := {}.
End RelCompFun_Instances.
@@ -160,6 +158,8 @@ Section RelProd_Instances.
Proof. unfold RelCompFun; firstorder. Qed.
End RelProd_Instances.
+#[global]
Hint Unfold RelProd RelCompFun : core.
+#[global]
Hint Extern 2 (RelProd _ _ _ _) => split : core.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 21:50:09 +0000