aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Unit.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/Unit.v')
-rw-r--r--src/Util/Unit.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/Unit.v b/src/Util/Unit.v
index cf5c4f669..637c3daeb 100644
--- a/src/Util/Unit.v
+++ b/src/Util/Unit.v
@@ -1,5 +1,5 @@
Require Import Coq.Classes.Morphisms.
-Require Import Relation_Definitions.
+Require Import Coq.Relations.Relation_Definitions.
(* an equivalence for a relation on trivial things, like [unit] *)
Global Instance Equivalence_trivial {A} : Equivalence (fun _ _ : A => True).