make sure we import 'options' everywhere

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

theories/algebra/big_op.v

 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.

theories/algebra/cmra_big_op.v

 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 :

theories/algebra/lib/excl_auth.v

 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]

theories/algebra/lib/frac_auth.v

 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

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)).

theories/algebra/numbers.v

 From iris.algebra Require Export cmra local_updates proofmode_classes.
+From iris Require Import options.
 
 (** ** Natural numbers with [add] as the operation. *)
 Section nat.

theories/algebra/proofmode_classes.v

 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:
 

theories/base_logic/bi.v

 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

theories/base_logic/bupd_alt.v

 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 [■]. *)

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.

theories/base_logic/proofmode.v

 From iris.algebra Require Import proofmode_classes.
 From iris.base_logic Require Export derived.
+From iris Require Import options.
 
 Import base_logic.bi.uPred.
 

theories/bi/ascii.v

 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.

theories/bi/derived_connectives.v

 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.

theories/bi/derived_laws.v

 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

theories/bi/derived_laws_later.v

 From iris.bi Require Export derived_laws.
 From iris.algebra Require Import monoid.
+From iris Require Import options.
 
 Module bi.
 Import interface.bi.

theories/bi/embedding.v

 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.

theories/bi/interface.v

 From iris.bi Require Export notation.
 From iris.algebra Require Export ofe.
+From iris Require Import options.
 Set Primitive Projections.
 
 Section bi_mixin.

theories/bi/internal_eq.v

 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.

theories/bi/lib/counterexamples.v

 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

theories/bi/lib/fixpoint.v

 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.
 

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)

theories/bi/monpred.v

 From stdpp Require Import coPset.
 From iris.bi Require Import bi.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** Definitions. *)
 Structure biIndex :=

theories/bi/notation.v

+From iris Require Import options.
 (** Just reserve the notation. *)
 
 (** * Turnstiles *)

theories/bi/plainly.v

 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.

theories/bi/telescopes.v

 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! *)

theories/bi/updates.v

 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.

theories/bi/weakestpre.v

 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.
 

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

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).
 

theories/heap_lang/lib/nondet_bool.v

 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".

theories/heap_lang/locations.v

 From stdpp Require Import countable numbers gmap.
 From iris.algebra Require Import base.
+From iris Require Import options.
 
 Record loc := { loc_car : Z }.
 

theories/heap_lang/metatheory.v

 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. *)

theories/heap_lang/proph_erasure.v

 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

theories/proofmode/ident_name.v

 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

theories/proofmode/monpred.v

 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) :=

theories/proofmode/reduction.v

 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

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.

theories/si_logic/bi.v

 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

theories/si_logic/siprop.v

 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