diff --git a/iris/prelude/options.v b/iris/prelude/options.v index 22d74e4a485069bc1cc8ce71dcf386d6e840b23a..cd6d5b0f3e04d341c94030c94e7fc240882a2122 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.