From eb376faed91dbce7dec7bca16b676bc0084555f1 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Thu, 3 Dec 2020 09:26:53 -0600
Subject: [PATCH] Make deprecated-hint-without-locality an error

---
 iris/prelude/options.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/iris/prelude/options.v b/iris/prelude/options.v
index 22d74e4a4..cd6d5b0f3 100644
--- a/iris/prelude/options.v
+++ b/iris/prelude/options.v
@@ -10,6 +10,10 @@ Export Set Suggest Proof Using. (* also warns about forgotten [Proof.] *)
 that bullets and curly braces must be used to structure the proof. *)
 Export Set Default Goal Selector "!".
 
+(* We always annotate hints with locality ([Global] or [Local]). This enforces
+that at least global hints are annotated. *)
+Export Set Warnings "+deprecated-hint-without-locality".
+
 (* "Fake" import to whitelist this file for the check that ensures we import
 this file everywhere.
 From iris.prelude Require Import options.
-- 
GitLab