From 9291076e30b14cd1a88c966266fb1973f58d7181 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 5 Sep 2020 12:55:46 +0200
Subject: [PATCH] make sure we import 'options' everywhere
---
Makefile.coq.local | 4 ++++
theories/algebra/big_op.v | 18 +++++++++---------
theories/algebra/cmra_big_op.v | 2 +-
theories/algebra/lib/excl_auth.v | 1 +
theories/algebra/lib/frac_auth.v | 1 +
theories/algebra/lib/ufrac_auth.v | 1 +
theories/algebra/numbers.v | 1 +
theories/algebra/proofmode_classes.v | 1 +
theories/base_logic/bi.v | 1 +
theories/base_logic/bupd_alt.v | 4 ++++
.../base_logic/lib/fancy_updates_from_vs.v | 3 +++
theories/base_logic/proofmode.v | 1 +
theories/bi/ascii.v | 1 +
theories/bi/derived_connectives.v | 1 +
theories/bi/derived_laws.v | 4 ++++
theories/bi/derived_laws_later.v | 1 +
theories/bi/embedding.v | 4 ++++
theories/bi/interface.v | 1 +
theories/bi/internal_eq.v | 1 +
theories/bi/lib/counterexamples.v | 3 +++
theories/bi/lib/fixpoint.v | 16 ++++++++--------
theories/bi/lib/relations.v | 4 ++++
theories/bi/monpred.v | 2 +-
theories/bi/notation.v | 1 +
theories/bi/plainly.v | 4 ++++
theories/bi/telescopes.v | 2 +-
theories/bi/updates.v | 4 ++++
theories/bi/weakestpre.v | 1 +
theories/heap_lang/lib/clairvoyant_coin.v | 1 +
theories/heap_lang/lib/lazy_coin.v | 1 +
theories/heap_lang/lib/nondet_bool.v | 1 +
theories/heap_lang/locations.v | 1 +
theories/heap_lang/metatheory.v | 1 +
theories/heap_lang/proph_erasure.v | 1 +
theories/proofmode/ident_name.v | 1 +
theories/proofmode/monpred.v | 1 +
theories/proofmode/reduction.v | 1 +
theories/proofmode/tactics.v | 1 +
theories/si_logic/bi.v | 1 +
theories/si_logic/siprop.v | 1 +
40 files changed, 80 insertions(+), 20 deletions(-)
diff --git a/Makefile.coq.local b/Makefile.coq.local
index f10e32d02..4d618052e 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -12,6 +12,10 @@ TESTFILES:=$(wildcard tests/*.v)
NORMALIZER:=test-normalizer.sed
test: $(TESTFILES:.v=.vo)
+# Make sure everything imports the options.
+ $(HIDE)for FILE in $$(find theories/ -name "*.v" | fgrep -v theories/options.v); do \
+ if ! fgrep -q 'From iris Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; exit 1; fi \
+ done
.PHONY: test
COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v
index aa4b02911..901e4159e 100644
--- a/theories/algebra/big_op.v
+++ b/theories/algebra/big_op.v
@@ -1,6 +1,6 @@
From stdpp Require Export functions gmap gmultiset.
From iris.algebra Require Export monoid.
-Set Default Proof Using "Type*".
+From iris Require Import options.
Local Existing Instances monoid_ne monoid_assoc monoid_comm
monoid_left_id monoid_right_id monoid_proper
monoid_homomorphism_rel_po monoid_homomorphism_rel_proper
@@ -619,36 +619,36 @@ Section homomorphisms.
Lemma big_opL_commute_L {A} (h : M1 → M2)
`{!MonoidHomomorphism o1 o2 (≡) h} (f : nat → A → M1) l :
h ([^o1 list] k↦x ∈ l, f k x) = ([^o2 list] k↦x ∈ l, h (f k x)).
- Proof. unfold_leibniz. by apply big_opL_commute. Qed.
+ Proof using Type*. unfold_leibniz. by apply big_opL_commute. Qed.
Lemma big_opL_commute1_L {A} (h : M1 → M2)
`{!WeakMonoidHomomorphism o1 o2 (≡) h} (f : nat → A → M1) l :
l ≠[] → h ([^o1 list] k↦x ∈ l, f k x) = ([^o2 list] k↦x ∈ l, h (f k x)).
- Proof. unfold_leibniz. by apply big_opL_commute1. Qed.
+ Proof using Type*. unfold_leibniz. by apply big_opL_commute1. Qed.
Lemma big_opM_commute_L `{Countable K} {A} (h : M1 → M2)
`{!MonoidHomomorphism o1 o2 (≡) h} (f : K → A → M1) m :
h ([^o1 map] k↦x ∈ m, f k x) = ([^o2 map] k↦x ∈ m, h (f k x)).
- Proof. unfold_leibniz. by apply big_opM_commute. Qed.
+ Proof using Type*. unfold_leibniz. by apply big_opM_commute. Qed.
Lemma big_opM_commute1_L `{Countable K} {A} (h : M1 → M2)
`{!WeakMonoidHomomorphism o1 o2 (≡) h} (f : K → A → M1) m :
m ≠∅ → h ([^o1 map] k↦x ∈ m, f k x) = ([^o2 map] k↦x ∈ m, h (f k x)).
- Proof. unfold_leibniz. by apply big_opM_commute1. Qed.
+ Proof using Type*. unfold_leibniz. by apply big_opM_commute1. Qed.
Lemma big_opS_commute_L `{Countable A} (h : M1 → M2)
`{!MonoidHomomorphism o1 o2 (≡) h} (f : A → M1) X :
h ([^o1 set] x ∈ X, f x) = ([^o2 set] x ∈ X, h (f x)).
- Proof. unfold_leibniz. by apply big_opS_commute. Qed.
+ Proof using Type*. unfold_leibniz. by apply big_opS_commute. Qed.
Lemma big_opS_commute1_L `{ Countable A} (h : M1 → M2)
`{!WeakMonoidHomomorphism o1 o2 (≡) h} (f : A → M1) X :
X ≠∅ → h ([^o1 set] x ∈ X, f x) = ([^o2 set] x ∈ X, h (f x)).
- Proof. intros. rewrite <-leibniz_equiv_iff. by apply big_opS_commute1. Qed.
+ Proof using Type*. intros. rewrite <-leibniz_equiv_iff. by apply big_opS_commute1. Qed.
Lemma big_opMS_commute_L `{Countable A} (h : M1 → M2)
`{!MonoidHomomorphism o1 o2 (≡) h} (f : A → M1) X :
h ([^o1 mset] x ∈ X, f x) = ([^o2 mset] x ∈ X, h (f x)).
- Proof. unfold_leibniz. by apply big_opMS_commute. Qed.
+ Proof using Type*. unfold_leibniz. by apply big_opMS_commute. Qed.
Lemma big_opMS_commute1_L `{Countable A} (h : M1 → M2)
`{!WeakMonoidHomomorphism o1 o2 (≡) h} (f : A → M1) X :
X ≠∅ → h ([^o1 mset] x ∈ X, f x) = ([^o2 mset] x ∈ X, h (f x)).
- Proof. intros. rewrite <-leibniz_equiv_iff. by apply big_opMS_commute1. Qed.
+ Proof using Type*. intros. rewrite <-leibniz_equiv_iff. by apply big_opMS_commute1. Qed.
End homomorphisms.
diff --git a/theories/algebra/cmra_big_op.v b/theories/algebra/cmra_big_op.v
index caae9ed56..edce5cb70 100644
--- a/theories/algebra/cmra_big_op.v
+++ b/theories/algebra/cmra_big_op.v
@@ -1,6 +1,6 @@
From stdpp Require Import gmap gmultiset.
From iris.algebra Require Export big_op cmra.
-Set Default Proof Using "Type*".
+From iris Require Import options.
(** Option *)
Lemma big_opL_None {M : cmraT} {A} (f : nat → A → option M) l :
diff --git a/theories/algebra/lib/excl_auth.v b/theories/algebra/lib/excl_auth.v
index baed9dd5b..9a0866583 100644
--- a/theories/algebra/lib/excl_auth.v
+++ b/theories/algebra/lib/excl_auth.v
@@ -1,6 +1,7 @@
From iris.algebra Require Export auth excl updates.
From iris.algebra Require Import local_updates.
From iris.base_logic Require Import base_logic.
+From iris Require Import options.
(** Authoritative CMRA where the fragment is exclusively owned.
This is effectively a single "ghost variable" with two views, the frament [â—¯E a]
diff --git a/theories/algebra/lib/frac_auth.v b/theories/algebra/lib/frac_auth.v
index 324de2eac..14cc4b58b 100644
--- a/theories/algebra/lib/frac_auth.v
+++ b/theories/algebra/lib/frac_auth.v
@@ -1,5 +1,6 @@
From iris.algebra Require Export frac auth updates local_updates.
From iris.algebra Require Import proofmode_classes.
+From iris Require Import options.
(** Authoritative CMRA where the NON-authoritative parts can be fractional.
This CMRA allows the original non-authoritative element [â—¯ a] to be split into
diff --git a/theories/algebra/lib/ufrac_auth.v b/theories/algebra/lib/ufrac_auth.v
index af7a5c07f..9020deebf 100644
--- a/theories/algebra/lib/ufrac_auth.v
+++ b/theories/algebra/lib/ufrac_auth.v
@@ -19,6 +19,7 @@ difference:
From Coq Require Import QArith Qcanon.
From iris.algebra Require Export auth frac updates local_updates.
From iris.algebra Require Import ufrac proofmode_classes.
+From iris Require Import options.
Definition ufrac_authR (A : cmraT) : cmraT :=
authR (optionUR (prodR ufracR A)).
diff --git a/theories/algebra/numbers.v b/theories/algebra/numbers.v
index e7443c7a2..b83e36f23 100644
--- a/theories/algebra/numbers.v
+++ b/theories/algebra/numbers.v
@@ -1,4 +1,5 @@
From iris.algebra Require Export cmra local_updates proofmode_classes.
+From iris Require Import options.
(** ** Natural numbers with [add] as the operation. *)
Section nat.
diff --git a/theories/algebra/proofmode_classes.v b/theories/algebra/proofmode_classes.v
index 2e42bebf5..608b329e4 100644
--- a/theories/algebra/proofmode_classes.v
+++ b/theories/algebra/proofmode_classes.v
@@ -1,5 +1,6 @@
From iris.algebra Require Export cmra.
From iris.proofmode Require Export classes.
+From iris Require Import options.
(* There are various versions of [IsOp] with different modes:
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 516274c02..593b6081f 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -1,5 +1,6 @@
From iris.bi Require Export derived_connectives updates internal_eq plainly.
From iris.base_logic Require Export upred.
+From iris Require Import options.
Import uPred_primitive.
(** BI instances for [uPred], and re-stating the remaining primitive laws in
diff --git a/theories/base_logic/bupd_alt.v b/theories/base_logic/bupd_alt.v
index 67d04dc7a..b40031111 100644
--- a/theories/base_logic/bupd_alt.v
+++ b/theories/base_logic/bupd_alt.v
@@ -1,5 +1,9 @@
From iris.proofmode Require Import tactics.
From iris.base_logic Require Export base_logic.
+From iris Require Import options.
+
+(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
+Set Default Proof Using "Type*".
(** This file contains an alternative version of basic updates, that is
expression in terms of just the plain modality [â– ]. *)
diff --git a/theories/base_logic/lib/fancy_updates_from_vs.v b/theories/base_logic/lib/fancy_updates_from_vs.v
index 80b52c855..4d3654f68 100644
--- a/theories/base_logic/lib/fancy_updates_from_vs.v
+++ b/theories/base_logic/lib/fancy_updates_from_vs.v
@@ -4,6 +4,9 @@ laws of the view shift. *)
From stdpp Require Export coPset.
From iris.proofmode Require Import tactics.
From iris.base_logic Require Export base_logic.
+From iris Require Import options.
+
+(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
Set Default Proof Using "Type*".
Section fupd.
diff --git a/theories/base_logic/proofmode.v b/theories/base_logic/proofmode.v
index c5eba535b..d9f3a0e98 100644
--- a/theories/base_logic/proofmode.v
+++ b/theories/base_logic/proofmode.v
@@ -1,5 +1,6 @@
From iris.algebra Require Import proofmode_classes.
From iris.base_logic Require Export derived.
+From iris Require Import options.
Import base_logic.bi.uPred.
diff --git a/theories/bi/ascii.v b/theories/bi/ascii.v
index 0f9559577..159f0b964 100644
--- a/theories/bi/ascii.v
+++ b/theories/bi/ascii.v
@@ -1,5 +1,6 @@
From iris.bi Require Import interface derived_connectives updates.
From iris.algebra Require Export ofe.
+From iris Require Import options.
Notation "P |- Q" := (P ⊢ Q)
(at level 99, Q at level 200, right associativity, only parsing) : stdpp_scope.
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index 0ca78688d..f75bddc20 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -1,5 +1,6 @@
From iris.bi Require Export interface.
From iris.algebra Require Import monoid.
+From iris Require Import options.
Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P → Q) ∧ (Q → P))%I.
Arguments bi_iff {_} _%I _%I : simpl never.
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 2a1bbc107..a9710b744 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -1,5 +1,9 @@
From iris.bi Require Export derived_connectives.
From iris.algebra Require Import monoid.
+From iris Require Import options.
+
+(* The sections add [BiAffine] and the like, which is only picked up with "Type"*. *)
+Set Default Proof Using "Type*".
(** Naming schema for lemmas about modalities:
M1_into_M2: M1 P ⊢ M2 P
diff --git a/theories/bi/derived_laws_later.v b/theories/bi/derived_laws_later.v
index b5c520709..06084c0be 100644
--- a/theories/bi/derived_laws_later.v
+++ b/theories/bi/derived_laws_later.v
@@ -1,5 +1,6 @@
From iris.bi Require Export derived_laws.
From iris.algebra Require Import monoid.
+From iris Require Import options.
Module bi.
Import interface.bi.
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 9862bcd95..8a8374852 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -1,6 +1,10 @@
From iris.bi Require Import interface derived_laws_later big_op.
From iris.bi Require Import plainly updates internal_eq.
From iris.algebra Require Import monoid.
+From iris Require Import options.
+
+(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
+Set Default Proof Using "Type*".
Class Embed (A B : Type) := embed : A → B.
Arguments embed {_ _ _} _%I : simpl never.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 25198a338..b0df9c757 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -1,5 +1,6 @@
From iris.bi Require Export notation.
From iris.algebra Require Export ofe.
+From iris Require Import options.
Set Primitive Projections.
Section bi_mixin.
diff --git a/theories/bi/internal_eq.v b/theories/bi/internal_eq.v
index 6ecd8ec6f..3ffb1d71f 100644
--- a/theories/bi/internal_eq.v
+++ b/theories/bi/internal_eq.v
@@ -1,4 +1,5 @@
From iris.bi Require Import derived_laws_later big_op.
+From iris Require Import options.
Import interface.bi derived_laws.bi derived_laws_later.bi.
(** This file defines a type class for BIs with a notion of internal equality.
diff --git a/theories/bi/lib/counterexamples.v b/theories/bi/lib/counterexamples.v
index 5f91cfe4f..3297952f2 100644
--- a/theories/bi/lib/counterexamples.v
+++ b/theories/bi/lib/counterexamples.v
@@ -1,5 +1,8 @@
From iris.bi Require Export bi.
From iris.proofmode Require Import tactics.
+From iris Require Import options.
+
+(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
Set Default Proof Using "Type*".
(** This proves that we need the â–· in a "Saved Proposition" construction with
diff --git a/theories/bi/lib/fixpoint.v b/theories/bi/lib/fixpoint.v
index 196d32b1d..8935289d8 100644
--- a/theories/bi/lib/fixpoint.v
+++ b/theories/bi/lib/fixpoint.v
@@ -1,6 +1,6 @@
From iris.bi Require Export bi.
From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+From iris Require Import options.
Import bi.
(** Least and greatest fixpoint of a monotone function, defined entirely inside
@@ -35,7 +35,7 @@ Section least.
Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
Lemma least_fixpoint_unfold_2 x : F (bi_least_fixpoint F) x ⊢ bi_least_fixpoint F x.
- Proof.
+ Proof using Type*.
rewrite /bi_least_fixpoint /=. iIntros "HF" (Φ) "#Hincl".
iApply "Hincl". iApply (bi_mono_pred _ Φ with "[#]"); last done.
iIntros "!>" (y) "Hy". iApply ("Hy" with "[# //]").
@@ -43,7 +43,7 @@ Section least.
Lemma least_fixpoint_unfold_1 x :
bi_least_fixpoint F x ⊢ F (bi_least_fixpoint F) x.
- Proof.
+ Proof using Type*.
iIntros "HF". iApply ("HF" $! (OfeMor (F (bi_least_fixpoint F))) with "[#]").
iIntros "!>" (y) "Hy /=". iApply (bi_mono_pred with "[#]"); last done.
iIntros "!>" (z) "?". by iApply least_fixpoint_unfold_2.
@@ -51,7 +51,7 @@ Section least.
Corollary least_fixpoint_unfold x :
bi_least_fixpoint F x ≡ F (bi_least_fixpoint F) x.
- Proof.
+ Proof using Type*.
apply (anti_symm _); auto using least_fixpoint_unfold_1, least_fixpoint_unfold_2.
Qed.
@@ -64,7 +64,7 @@ Section least.
Lemma least_fixpoint_strong_ind (Φ : A → PROP) `{!NonExpansive Φ} :
□ (∀ y, F (λ x, Φ x ∧ bi_least_fixpoint F x) y -∗ Φ y) -∗
∀ x, bi_least_fixpoint F x -∗ Φ x.
- Proof.
+ Proof using Type*.
trans (∀ x, bi_least_fixpoint F x -∗ Φ x ∧ bi_least_fixpoint F x)%I.
{ iIntros "#HΦ". iApply (least_fixpoint_ind with "[]"); first solve_proper.
iIntros "!>" (y) "H". iSplit; first by iApply "HΦ".
@@ -97,7 +97,7 @@ Section greatest.
Lemma greatest_fixpoint_unfold_1 x :
bi_greatest_fixpoint F x ⊢ F (bi_greatest_fixpoint F) x.
- Proof.
+ Proof using Type*.
iDestruct 1 as (Φ) "[#Hincl HΦ]".
iApply (bi_mono_pred Φ (bi_greatest_fixpoint F) with "[#]").
- iIntros "!>" (y) "Hy". iExists Φ. auto.
@@ -106,7 +106,7 @@ Section greatest.
Lemma greatest_fixpoint_unfold_2 x :
F (bi_greatest_fixpoint F) x ⊢ bi_greatest_fixpoint F x.
- Proof.
+ Proof using Type*.
iIntros "HF". iExists (OfeMor (F (bi_greatest_fixpoint F))).
iSplit; last done. iIntros "!>" (y) "Hy /=". iApply (bi_mono_pred with "[#] Hy").
iIntros "!>" (z) "?". by iApply greatest_fixpoint_unfold_1.
@@ -114,7 +114,7 @@ Section greatest.
Corollary greatest_fixpoint_unfold x :
bi_greatest_fixpoint F x ≡ F (bi_greatest_fixpoint F) x.
- Proof.
+ Proof using Type*.
apply (anti_symm _); auto using greatest_fixpoint_unfold_1, greatest_fixpoint_unfold_2.
Qed.
diff --git a/theories/bi/lib/relations.v b/theories/bi/lib/relations.v
index a42b93d8b..11f5d6aa7 100644
--- a/theories/bi/lib/relations.v
+++ b/theories/bi/lib/relations.v
@@ -2,6 +2,10 @@
its reflexive transitive closure. *)
From iris.bi.lib Require Export fixpoint.
From iris.proofmode Require Import tactics.
+From iris Require Import options.
+
+(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
+Set Default Proof Using "Type*".
Definition bi_rtc_pre `{!BiInternalEq PROP}
{A : ofeT} (R : A → A → PROP)
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 7202ef375..f5a13ea17 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -1,6 +1,6 @@
From stdpp Require Import coPset.
From iris.bi Require Import bi.
-Set Default Proof Using "Type".
+From iris Require Import options.
(** Definitions. *)
Structure biIndex :=
diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index d67cc7f89..bea7f6b41 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -1,3 +1,4 @@
+From iris Require Import options.
(** Just reserve the notation. *)
(** * Turnstiles *)
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index b81fe05d1..95a1dd5c8 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -1,7 +1,11 @@
From iris.bi Require Import derived_laws_later big_op internal_eq.
From iris.algebra Require Import monoid.
+From iris Require Import options.
Import interface.bi derived_laws.bi derived_laws_later.bi.
+(* The sections add [BiAffine] and the like, which is only picked up with "Type"*. *)
+Set Default Proof Using "Type*".
+
Class Plainly (A : Type) := plainly : A → A.
Arguments plainly {A}%type_scope {_} _%I.
Hint Mode Plainly ! : typeclass_instances.
diff --git a/theories/bi/telescopes.v b/theories/bi/telescopes.v
index 9c934356e..2bef8b0e7 100644
--- a/theories/bi/telescopes.v
+++ b/theories/bi/telescopes.v
@@ -1,6 +1,6 @@
From stdpp Require Export telescopes.
From iris.bi Require Export bi.
-Set Default Proof Using "Type*".
+From iris Require Import options.
Import bi.
(* This cannot import the proofmode because it is imported by the proofmode! *)
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 9690d30af..5c87a174d 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -1,7 +1,11 @@
From stdpp Require Import coPset.
From iris.bi Require Import interface derived_laws_later big_op plainly.
+From iris Require Import options.
Import interface.bi derived_laws.bi derived_laws_later.bi.
+(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
+Set Default Proof Using "Type*".
+
(* We first define operational type classes for the notations, and then later
bundle these operational type classes with the laws. *)
Class BUpd (PROP : Type) : Type := bupd : PROP → PROP.
diff --git a/theories/bi/weakestpre.v b/theories/bi/weakestpre.v
index d6de4370c..ee7181d5c 100644
--- a/theories/bi/weakestpre.v
+++ b/theories/bi/weakestpre.v
@@ -1,6 +1,7 @@
From stdpp Require Export coPset.
From iris.bi Require Import interface derived_connectives.
From iris.program_logic Require Import language.
+From iris Require Import options.
Inductive stuckness := NotStuck | MaybeStuck.
diff --git a/theories/heap_lang/lib/clairvoyant_coin.v b/theories/heap_lang/lib/clairvoyant_coin.v
index a865289ba..70673ad50 100644
--- a/theories/heap_lang/lib/clairvoyant_coin.v
+++ b/theories/heap_lang/lib/clairvoyant_coin.v
@@ -2,6 +2,7 @@ From iris.base_logic Require Export invariants.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang.lib Require Export nondet_bool.
+From iris Require Import options.
(** The clairvoyant coin predicts all the values that it will
*non-deterministically* choose throughout the execution of the
diff --git a/theories/heap_lang/lib/lazy_coin.v b/theories/heap_lang/lib/lazy_coin.v
index b22c0707a..315cc5f3f 100644
--- a/theories/heap_lang/lib/lazy_coin.v
+++ b/theories/heap_lang/lib/lazy_coin.v
@@ -2,6 +2,7 @@ From iris.base_logic Require Export invariants.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang.lib Require Export nondet_bool.
+From iris Require Import options.
Definition new_coin: val := λ: <>, (ref NONE, NewProph).
diff --git a/theories/heap_lang/lib/nondet_bool.v b/theories/heap_lang/lib/nondet_bool.v
index fcf7f6a03..98aec67e0 100644
--- a/theories/heap_lang/lib/nondet_bool.v
+++ b/theories/heap_lang/lib/nondet_bool.v
@@ -1,6 +1,7 @@
From iris.base_logic Require Export invariants.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
+From iris Require Import options.
Definition nondet_bool : val :=
λ: <>, let: "l" := ref #true in Fork ("l" <- #false);; !"l".
diff --git a/theories/heap_lang/locations.v b/theories/heap_lang/locations.v
index 4f4df7d12..146b3816a 100644
--- a/theories/heap_lang/locations.v
+++ b/theories/heap_lang/locations.v
@@ -1,5 +1,6 @@
From stdpp Require Import countable numbers gmap.
From iris.algebra Require Import base.
+From iris Require Import options.
Record loc := { loc_car : Z }.
diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v
index 5ff1dcb67..106a12423 100644
--- a/theories/heap_lang/metatheory.v
+++ b/theories/heap_lang/metatheory.v
@@ -1,5 +1,6 @@
From stdpp Require Import gmap.
From iris.heap_lang Require Export lang.
+From iris Require Import options.
(* This file contains some metatheory about the heap_lang language,
which is not needed for verifying programs. *)
diff --git a/theories/heap_lang/proph_erasure.v b/theories/heap_lang/proph_erasure.v
index a568a68c3..4cfeef1bc 100644
--- a/theories/heap_lang/proph_erasure.v
+++ b/theories/heap_lang/proph_erasure.v
@@ -1,5 +1,6 @@
From iris.program_logic Require Export adequacy.
From iris.heap_lang Require Export lang notation tactics.
+From iris Require Import options.
(** This file contains the proof that prophecies can be safely erased
from programs. We erase a program by replacing prophecy identifiers
diff --git a/theories/proofmode/ident_name.v b/theories/proofmode/ident_name.v
index c79e67e81..136493f13 100644
--- a/theories/proofmode/ident_name.v
+++ b/theories/proofmode/ident_name.v
@@ -1,4 +1,5 @@
From stdpp Require Import base.
+From iris Require Import options.
(** [ident_name] is a way to remember an identifier within the binder of a
(trivial) function, which can be constructed and retrieved with Ltac but is easy
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 909b7324c..93983d9d9 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -1,6 +1,7 @@
From iris.bi Require Export monpred.
From iris.bi Require Import plainly.
From iris.proofmode Require Import tactics modality_instances.
+From iris Require Import options.
Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
(P : monPred I PROP) (ð“Ÿ : PROP) :=
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index c9d616778..c92ba206b 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -1,5 +1,6 @@
From iris.bi Require Import bi telescopes.
From iris.proofmode Require Import base environments.
+From iris Require Import options.
(** Called by all tactics to perform computation to lookup items in the
context. We avoid reducing anything user-visible here to make sure we
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 636885cb8..6fdca9b1e 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -5,3 +5,4 @@ From iris.proofmode Require Import class_instances class_instances_later
class_instances_updates class_instances_embedding
class_instances_plainly class_instances_internal_eq.
From iris.proofmode Require Import frame_instances modality_instances.
+From iris Require Import options.
diff --git a/theories/si_logic/bi.v b/theories/si_logic/bi.v
index 8392463e4..d9cc4ae66 100644
--- a/theories/si_logic/bi.v
+++ b/theories/si_logic/bi.v
@@ -1,5 +1,6 @@
From iris.bi Require Export bi.
From iris.si_logic Require Export siprop.
+From iris Require Import options.
Import siProp_primitive.
(** BI instances for [siProp], and re-stating the remaining primitive laws in
diff --git a/theories/si_logic/siprop.v b/theories/si_logic/siprop.v
index 1ea1bde1f..cddd84898 100644
--- a/theories/si_logic/siprop.v
+++ b/theories/si_logic/siprop.v
@@ -1,5 +1,6 @@
From iris.algebra Require Export ofe.
From iris.bi Require Import notation.
+From iris Require Import options.
(** The type [siProp] defines "plain" step-indexed propositions, on which we
define the usual connectives of higher-order logic, and prove that these satisfy
--
GitLab