From 68cd077344ce37db1a601079dbc4fdcae6c8d41f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 14 Nov 2020 17:55:07 +0100
Subject: Explicitly annotate all hint declarations of the standard library.

By default Coq stdlib warnings raise an error, so this is really required.
---
 theories/Program/Basics.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'theories/Program/Basics.v')

diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 3e282f696a..3ecb5a5a61 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -26,6 +26,7 @@ Arguments id {A} x.
 Definition compose {A B C} (g : B -> C) (f : A -> B) :=
   fun x : A => g (f x).
 
+#[global]
 Hint Unfold compose : core.
 
 Declare Scope program_scope.
-- 
cgit v1.2.3