aboutsummaryrefslogtreecommitdiff
path: root/theories/Structures/Orders.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Structures/Orders.v')
-rw-r--r--theories/Structures/Orders.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
index 42756ad339..310a22a0a4 100644
--- a/theories/Structures/Orders.v
+++ b/theories/Structures/Orders.v
@@ -181,7 +181,7 @@ Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder
we coerce [bool] into [Prop]. *)
Local Coercion is_true : bool >-> Sortclass.
-Hint Unfold is_true.
+Hint Unfold is_true : core.
Module Type HasLeb (Import T:Typ).
Parameter Inline leb : t -> t -> bool.