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/Equality.v | 2 ++
 1 file changed, 2 insertions(+)

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

diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 5862a08838..25af2d5ffb 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -21,6 +21,7 @@ Ltac is_ground_goal :=
 
 (** Try to find a contradiction. *)
 
+#[global]
 Hint Extern 10 => is_ground_goal ; progress exfalso : exfalso.
 
 (** We will use the [block] definition to separate the goal from the 
@@ -308,6 +309,7 @@ Proof. intros. rewrite (UIP_refl A). assumption. Defined.
 (** This hint database and the following tactic can be used with [autounfold] to 
    unfold everything to [eq_rect]s. *)
 
+#[global]
 Hint Unfold solution_left solution_right deletion simplification_heq
   simplification_existT1 simplification_existT2 simplification_K
   eq_rect_r eq_rec eq_ind : dep_elim.
-- 
cgit v1.2.3