aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures/GenericMinMax.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Structures/GenericMinMax.v')
-rw-r--r--theories/Structures/GenericMinMax.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index 68f201897..3b7dea5e4 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -7,6 +7,7 @@
(***********************************************************************)
Require Import Orders OrdersTac OrdersFacts Setoid Morphisms Basics.
+Import Morphisms_Prop. (* For Hints *)
(** * A Generic construction of min and max *)