use options file everywhere that we so far set 'Proof using'

theories/algebra/agree.v

 From iris.algebra Require Export cmra.
 From iris.algebra Require Import list.
 From iris.base_logic Require Import base_logic.
+From iris Require Import options.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 Local Arguments op _ _ _ !_ /.
@@ -50,7 +51,6 @@ Proof.
 Qed.
 
 Section agree.
-Local Set Default Proof Using "Type".
 Context {A : ofeT}.
 Implicit Types a b : A.
 Implicit Types x y : agree A.
@@ -276,7 +276,7 @@ Section agree_map.
   Context {A B : ofeT} (f : A → B) {Hf: NonExpansive f}.
 
   Instance agree_map_ne : NonExpansive (agree_map f).
-  Proof.
+  Proof using Type*.
     intros n x y [H H']; split=> b /=; setoid_rewrite elem_of_list_fmap.
     - intros (a&->&?). destruct (H a) as (a'&?&?); auto. naive_solver.
     - intros (a&->&?). destruct (H' a) as (a'&?&?); auto. naive_solver.

theories/algebra/auth.v

@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Export frac agree local_updates.
 From iris.algebra Require Import proofmode_classes.
 From iris.base_logic Require Import base_logic.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** Authoritative CMRA with fractional authoritative parts. [auth] has 3 types
   of elements: the fractional authoritative `●{q} a`, the full authoritative

theories/algebra/base.v

 From Coq.ssr Require Export ssreflect.
 From stdpp Require Export prelude.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Global Open Scope general_if_scope.
 Global Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *)
 Ltac done := stdpp.tactics.done.

theories/algebra/cmra.v

 From stdpp Require Import finite.
 From iris.algebra Require Export ofe monoid.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Class PCore (A : Type) := pcore : A → option A.
 Hint Mode PCore ! : typeclass_instances.

theories/algebra/coPset.v

 From stdpp Require Export sets coPset.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
-Set Default Proof Using "Type".
+From iris Require Import options.
 (** This is pretty much the same as algebra/gset, but I was not able to
 generalize the construction without breaking canonical structures. *)
 

theories/algebra/cofe_solver.v

 From iris.algebra Require Export ofe.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Record solution (F : oFunctor) := Solution {
   solution_car :> ofeT;

theories/algebra/csum.v

 From iris.algebra Require Export cmra.
 From iris.algebra Require Import local_updates.
 From iris.base_logic Require Import base_logic.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Local Arguments pcore _ _ !_ /.
 Local Arguments cmra_pcore _ !_ /.
 Local Arguments validN _ _ _ !_ /.

theories/algebra/dra.v

 From iris.algebra Require Export cmra updates.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Record DraMixin A `{Equiv A, PCore A, Disjoint A, Op A, Valid A} := {
   (* setoids *)

theories/algebra/excl.v

 From iris.algebra Require Export cmra.
 From iris.base_logic Require Import base_logic.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 

theories/algebra/frac.v

@@ -6,7 +6,7 @@ validity of the unbounded fractional camera [ufrac]. *)
 From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import proofmode_classes.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** Since the standard (0,1] fractional camera is used more often, we define
 [frac] through a [Notation] instead of a [Definition]. That way, Coq infers the

theories/algebra/functions.v

 From stdpp Require Import finite.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Definition discrete_fun_insert `{EqDecision A} {B : A → ofeT}
     (x : A) (y : B x) (f : discrete_fun B) : discrete_fun B := λ x',

theories/algebra/gmap.v

@@ -2,7 +2,7 @@ From stdpp Require Export list gmap.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates proofmode_classes.
 From iris.base_logic Require Import base_logic.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Section cofe.
 Context `{Countable K} {A : ofeT}.

theories/algebra/gmultiset.v

 From stdpp Require Export sets gmultiset countable.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (* The multiset union CMRA *)
 Section gmultiset.

theories/algebra/gset.v

 From stdpp Require Export sets gmap mapset.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (* The union CMRA *)
 Section gset.

theories/algebra/list.v

@@ -2,7 +2,7 @@ From stdpp Require Export list.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
 From iris.base_logic Require Import base_logic.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Section cofe.
 Context {A : ofeT}.

theories/algebra/local_updates.v

 From iris.algebra Require Export cmra.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** * Local updates *)
 Definition local_update {A : cmraT} (x y : A * A) := ∀ n mz,

theories/algebra/monoid.v

 From iris.algebra Require Export ofe.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** The Monoid class that is used for generic big operators in the file
 [algebra/big_op]. The operation is an argument because we want to have multiple

theories/algebra/namespace_map.v

 From stdpp Require Import namespaces.
 From iris.algebra Require Export gmap coPset local_updates.
 From iris.algebra Require Import updates proofmode_classes.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** The camera [namespace_map A] over a camera [A] provides the connectives
 [namespace_map_data N a], which associates data [a : A] with a namespace [N],

theories/algebra/ofe.v

 From iris.algebra Require Export base.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Set Primitive Projections.
 
 (** This files defines (a shallow embedding of) the category of OFEs:

theories/algebra/sts.v

 From stdpp Require Export propset.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import dra.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Local Arguments valid _ _ !_ /.
 Local Arguments op _ _ !_ !_ /.
 Local Arguments core _ _ !_ /.