Skip to content
Snippets Groups Projects
Verified Commit eb376fae authored by Tej Chajed's avatar Tej Chajed
Browse files

Make deprecated-hint-without-locality an error

parent 247db01f
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 4 additions and 0 deletions
iris/prelude/options.v
+ 4
− 0
View file @ eb376fae
...@@ -10,6 +10,10 @@ Export Set Suggest Proof Using. (* also warns about forgotten [Proof.] *) ...@@ -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. *) that bullets and curly braces must be used to structure the proof. *)
Export Set Default Goal Selector "!". 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 (* "Fake" import to whitelist this file for the check that ensures we import
this file everywhere. this file everywhere.
From iris.prelude Require Import options. From iris.prelude Require Import options.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment