import options in tests

tests/algebra.v

 From iris.algebra Require Import auth excl lib.gmap_view.
 From iris.base_logic.lib Require Import invariants.
+From iris.prelude Require Import options.
 
 Section test_dist_equiv_mode.
   (* check that the mode for [Dist] does not trigger https://github.com/coq/coq/issues/14441.

tests/atomic.v

 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export atomic.
 From iris.heap_lang Require Import proofmode notation atomic_heap.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 

tests/heap_lang.v

@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.heap_lang Require Import lang adequacy proofmode notation.
 (* Import lang *again*. This used to break notation. *)
 From iris.heap_lang Require Import lang.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
@@ -196,7 +196,7 @@ Section tests.
     val_is_unboxed v →
     l ↦ v -∗ WP CmpXchg #l v v {{ _, True }}.
   Proof.
-    iIntros (?) "?". wp_cmpxchg as ? | ?. done. done.
+    iIntros (?) "?". wp_cmpxchg as ? | ?; done.
   Qed.
 
   Lemma wp_xchg l (v₁ v₂ : val) :
@@ -478,5 +478,6 @@ Section error_tests.
   Abort.
 End error_tests.
 
+(* Test a closed proof *)
 Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (λ v _, v = #2).
 Proof. eapply (heap_adequacy heapΣ)=> ?. iIntros "_". by iApply heap_e_spec. Qed.

tests/heap_lang2.v

@@ -3,7 +3,7 @@ printing *)
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Export primitive_laws notation.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 

tests/heap_lang_proph.v

 From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.heap_lang Require Import lang adequacy proofmode notation.
-From iris.heap_lang Require Import lang.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Section tests.
   Context `{!heapGS Σ}.
@@ -16,7 +15,14 @@ Section tests.
   Proof.
     iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
     wp_cmpxchg_suc. iIntros "!>" (ws ->) "Hp". eauto with iFrame.
-  Restart.
+  Qed.
+
+  Lemma test_resolve1' E (l : loc) (n : Z) (p : proph_id) (vs : list (val * val)) (v : val) :
+    l ↦ #n -∗
+    proph p vs -∗
+    WP Resolve (CmpXchg #l #n (#n + #1)) #p v @ E
+      {{ v, ⌜v = (#n, #true)%V⌝ ∗ ∃vs, proph p vs ∗ l ↦ #(n+1) }}.
+  Proof.
     iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve_cmpxchg_suc with "[$Hp $Hl]"); first by left.
     iIntros "Hpost". iDestruct "Hpost" as (ws ->) "Hp". eauto with iFrame.
   Qed.

tests/heapprop.v

 From stdpp Require Import gmap.
 From iris.bi Require Import interface.
 From iris.proofmode Require Import tactics.
+From iris.prelude Require Import options.
 
 (** This file constructs a simple non step-indexed linear separation logic as
 predicates over heaps (modeled as maps from integer locations to integer values).

tests/ipm_paper.ref

@@ -14,7 +14,7 @@
   --------------------------------------∗
   Ψ x ∗ P
   
-2 goals
+1 goal
   
   M : ucmra
   A : Type
@@ -26,13 +26,6 @@
   --------------------------------------∗
   Ψ x
   
-
-goal 2 is:
- "HP" : P
-"HR" : R
---------------------------------------∗
-P
-
 1 goal
   
   M : ucmra

tests/ipm_paper.v

@@ -7,7 +7,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import base_logic.
 From iris.deprecated.program_logic Require Import hoare.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
@@ -23,7 +23,9 @@ Section demo.
     intros [HP [HΨ HR]].
     destruct HΨ as [x HΨ].
     exists x.
-    split. assumption. assumption.
+    split.
+    -  assumption.
+    -  assumption.
   Qed.
 
   (* The version in IPM *)
@@ -34,7 +36,9 @@ Section demo.
     iIntros "[HP [HΨ HR]]".
     iDestruct "HΨ" as (x) "HΨ".
     iExists x. Show.
-    iSplitL "HΨ". Show. iAssumption. Show. iAssumption.
+    iSplitL "HΨ".
+    - Show. iAssumption.
+    - Show. iAssumption.
   Qed.
 
   (* The short version in IPM, as in the paper *)
@@ -174,7 +178,7 @@ Section M.
   Global Instance frag_core_id n : CoreId (Frag n).
   Proof. by constructor. Qed.
   Lemma auth_frag_valid j n : ✓ (Auth n ⋅ Frag j) → j ≤ n.
-  Proof. simpl. case_decide. done. by intros []. Qed.
+  Proof. simpl. case_decide; first done. by intros []. Qed.
   Lemma auth_frag_op (j n : nat) : j ≤ n → Auth n = Auth n ⋅ Frag j.
   Proof. intros. by rewrite /= decide_True. Qed.
 

tests/list_reverse.v

@@ -3,7 +3,7 @@ From iris.proofmode Require Export tactics.
 From iris.program_logic Require Export total_weakestpre weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 

tests/mosel_paper.v

@@ -7,6 +7,7 @@ Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
 ICFP 2018 *)
 From iris.bi Require Import monpred.
 From iris.proofmode Require Import tactics monpred.
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 

tests/one_shot.v

@@ -5,7 +5,7 @@ From iris.deprecated.program_logic Require Import hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import assert proofmode notation adequacy.
 From iris.heap_lang.lib Require Import par.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 (** This is the introductory example from the "Iris from the Ground Up" journal
 paper. *)
@@ -76,8 +76,12 @@ Proof.
     iAssert (one_shot_inv γ l ∗ (⌜v = NONEV⌝ ∨ ∃ n : Z,
       ⌜v = SOMEV #n⌝ ∗ own γ (Shot n)))%I with "[Hl Hv]" as "[Hinv #Hv]".
     { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
-      + Show. iSplit. iLeft; by iSplitL "Hl". eauto.
-      + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
+      + Show. iSplit.
+        * iLeft; by iSplitL "Hl".
+        * eauto.
+      + iSplit.
+        * iRight; iExists m; by iSplitL "Hl".
+        * eauto. }
     iSplitL "Hinv"; first by eauto.
     iModIntro. wp_pures. iIntros "!> !>". wp_lam.
     iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']";

tests/one_shot_once.v

@@ -5,7 +5,7 @@ From iris.deprecated.program_logic Require Import hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import assert proofmode notation adequacy.
 From iris.heap_lang.lib Require Import par.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 (** This is the introductory example from Ralf's PhD thesis.
 The difference to [one_shot] is that [set] asserts to be called only once. *)
@@ -92,8 +92,12 @@ Proof.
     iAssert (one_shot_inv γ l ∗ (⌜v = NONEV⌝ ∨ ∃ n : Z,
       ⌜v = SOMEV #n⌝ ∗ own γ (Shot n)))%I with "[Hl Hv]" as "[Hinv #Hv]".
     { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
-      + Show. iSplit. iLeft; by iSplitL "Hl". eauto.
-      + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
+      + Show. iSplit.
+        * iLeft; by iSplitL "Hl".
+        * eauto.
+      + iSplit.
+        * iRight; iExists m; by iSplitL "Hl".
+        * eauto. }
     iSplitL "Hinv"; first by eauto.
     iModIntro. wp_pures. iIntros "!> !>". wp_lam. wp_bind (! _)%E.
     iInv N as "Hinv".

tests/proofmode.v

 From iris.bi Require Import laterable.
 From iris.proofmode Require Import tactics intro_patterns.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
@@ -28,7 +28,7 @@ Proof.
   (* should remove the disjunction "H" *)
   iDestruct "H" as "[#?|#?]"; last by iLeft. Show.
   (* should keep the disjunction "H" because it is instantiated *)
-  iDestruct ("H2" $! 10) as "[%|%]". done. done.
+  iDestruct ("H2" $! 10) as "[%|%]"; done.
 Qed.
 
 Lemma demo_2 P1 P2 P3 P4 Q (P5 : nat → PROP) `{!Affine P4, !Absorbing P2} :
@@ -46,7 +46,7 @@ Proof.
   (* split takes a list of hypotheses just for the LHS *)
   iSplitL "H3".
   - iFrame "H3". iRight. auto.
-  - iSplitL "HQ". iAssumption. by iSplitL "H1".
+  - iSplitL "HQ"; first iAssumption. by iSplitL "H1".
 Qed.
 
 Lemma demo_3 P1 P2 P3 :
@@ -719,7 +719,11 @@ Proof. iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ". Qed.
 
 Lemma test_iAlways P Q R :
   □ P -∗ <pers> Q → R -∗ <pers> <affine> <affine> P ∗ □ Q.
-Proof. iIntros "#HP #HQ HR". iSplitL. iModIntro. done. iModIntro. done. Qed.
+Proof.
+  iIntros "#HP #HQ HR". iSplitL.
+  - iModIntro. done.
+  - iModIntro. done.
+Qed.
 
 (* A bunch of test cases from #127 to establish that tactics behave the same on
 `⌜ φ ⌝ → P` and `∀ _ : φ, P` *)
@@ -731,7 +735,7 @@ Lemma test_forall_nondep_2 (φ : Prop) :
 Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
 Lemma test_forall_nondep_3 (φ : Prop) :
   φ → (∀ _ : φ, False : PROP) -∗ False.
-Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
+Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _); done. Qed.
 Lemma test_forall_nondep_4 (φ : Prop) :
   φ → (∀ _ : φ, False : PROP) -∗ False.
 Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ); done. Qed.
@@ -744,7 +748,7 @@ Lemma test_pure_impl_2 (φ : Prop) :
 Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
 Lemma test_pure_impl_3 (φ : Prop) :
   φ → (⌜φ⌝ → False : PROP) -∗ False.
-Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
+Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _); done. Qed.
 Lemma test_pure_impl_4 (φ : Prop) :
   φ → (⌜φ⌝ → False : PROP) -∗ False.
 Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ). done. Qed.
@@ -901,24 +905,32 @@ Qed.
 Lemma iFrame_with_evar_r P Q :
   ∃ R, (P -∗ Q -∗ P ∗ R) ∧ R = Q.
 Proof.
-  eexists. split. iIntros "HP HQ". iFrame. iApply "HQ". done.
+  eexists. split.
+  - iIntros "HP HQ". iFrame. iApply "HQ".
+  - done.
 Qed.
 Lemma iFrame_with_evar_l P Q :
   ∃ R, (P -∗ Q -∗ R ∗ P) ∧ R = Q.
 Proof.
-  eexists. split. iIntros "HP HQ". Fail iFrame "HQ".
-  iSplitR "HP"; iAssumption. done.
+  eexists. split.
+  - iIntros "HP HQ". Fail iFrame "HQ".
+    iSplitR "HP"; iAssumption.
+  - done.
 Qed.
 Lemma iFrame_with_evar_persistent P Q :
   ∃ R, (P -∗ □ Q -∗ P ∗ R ∗ Q) ∧ R = emp%I.
 Proof.
-  eexists. split. iIntros "HP #HQ". iFrame "HQ HP". iEmpIntro. done.
+  eexists. split.
+  - iIntros "HP #HQ". iFrame "HQ HP". iEmpIntro.
+  - done.
 Qed.
 
 Lemma test_iAccu P Q R S :
   ∃ PP, (□P -∗ Q -∗ R -∗ S -∗ PP) ∧ PP = (Q ∗ R ∗ S)%I.
 Proof.
-  eexists. split. iIntros "#? ? ? ?". iAccu. done.
+  eexists. split.
+  - iIntros "#? ? ? ?". iAccu.
+  - done.
 Qed.
 
 Lemma test_iAssumption_evar P : ∃ R, (R ⊢ P) ∧ R = P.

tests/proofmode_ascii.v

 From iris.proofmode Require Import tactics monpred.
 From iris.base_logic Require Import base_logic.
 From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
+From iris.prelude Require Import options.
 
 From iris.bi Require Import ascii.
 
-Set Default Proof Using "Type".
 Unset Mangle Names.
 
 (* Remove this and the [Set Printing Raw Literals.] below once we require Coq
@@ -36,7 +36,7 @@ Section base_logic_tests.
     iExists (S j + z1), z2.
     iNext.
     iApply ("H3" $! _ 0 with "[$]").
-    - iSplit. done. iApply "H2". iLeft. iApply "H2". by iRight.
+    - iSplit; first done. iApply "H2". iLeft. iApply "H2". by iRight.
     - done.
   Qed.
 

tests/proofmode_iris.v

@@ -2,6 +2,7 @@ From iris.algebra Require Import frac.
 From iris.proofmode Require Import tactics monpred.
 From iris.base_logic Require Import base_logic.
 From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
@@ -30,7 +31,7 @@ Section base_logic_tests.
     iExists (S j + z1), z2.
     iNext.
     iApply ("H3" $! _ 0 with "[$]").
-    - iSplit. done. iApply "H2". iLeft. iApply "H2". by iRight.
+    - iSplit; first done. iApply "H2". iLeft. iApply "H2". by iRight.
     - done.
   Qed.
 

tests/proofmode_monpred.v

 From iris.proofmode Require Import tactics monpred.
 From iris.base_logic.lib Require Import invariants.
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 

tests/proofmode_siprop.v

 From iris.proofmode Require Import tactics.
 From iris.si_logic Require Import bi.
+From iris.prelude Require Import options.
 
 Section si_logic_tests.
   Implicit Types P Q R : siProp.

tests/string_ident.v

 From iris.proofmode Require Import string_ident.
 From Coq Require Import Strings.String.
 From stdpp Require Import base.
-Open Scope string.
+Local Open Scope string.
 
 Lemma test_basic_ident : ∀ (n:nat), n = n.
 Proof.

tests/telescopes.v

 From stdpp Require Import coPset namespaces.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 

tests/tree_sum.v

@@ -2,7 +2,7 @@ From iris.proofmode Require Export tactics.
 From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Inductive tree :=
   | leaf : Z → tree