aboutsummaryrefslogtreecommitdiff
path: root/theories/Relations/Relation_Definitions.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Relations/Relation_Definitions.v')
-rw-r--r--theories/Relations/Relation_Definitions.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v
index 7d0dffdd00..d0d633a0c4 100644
--- a/theories/Relations/Relation_Definitions.v
+++ b/theories/Relations/Relation_Definitions.v
@@ -68,10 +68,13 @@ Section Relation_Definition.
End Relation_Definition.
+#[global]
Hint Unfold reflexive transitive antisymmetric symmetric: sets.
+#[global]
Hint Resolve Build_preorder Build_order Build_equivalence Build_PER
preord_refl preord_trans ord_refl ord_trans ord_antisym equiv_refl
equiv_trans equiv_sym per_sym per_trans: sets.
+#[global]
Hint Unfold inclusion same_relation commut: sets.