diff --git a/theories/examples/hashtable.v b/theories/examples/hashtable.v
index e8007239b2ccd4750956845a1aea2b7687501f65..fb7258d1bb3e79aad2deb33e05e744f128b96a37 100644
--- a/theories/examples/hashtable.v
+++ b/theories/examples/hashtable.v
@@ -74,13 +74,12 @@ Section hashtable.
 
 Definition const := 654435761.
 
-Instance hf1 : hash_fun := { size := Z.to_nat 16384; hash i := Z.to_nat ((i * const) mod 16384) }.
-Proof.
-  - hnf.
-    by apply (Z2Nat.inj_le 1 16384); compute.
-  - intro.
-    lapply (Z_mod_lt (i * const) 16384); last by compute.
-    by intros []; split; [apply (Z2Nat.inj_le 0) | apply (Z2Nat.inj_lt _ 16384)].
+Program Instance hf1 : hash_fun :=
+  { size := Z.to_nat 16384; hash i := Z.to_nat ((i * const) mod 16384) }.
+Next Obligation. hnf. by apply (Z2Nat.inj_le 1 16384); compute. Defined.
+Next Obligation.
+  intro. lapply (Z_mod_lt (i * const) 16384); last by compute.
+  by intros []; split; [apply (Z2Nat.inj_le 0) | apply (Z2Nat.inj_lt _ 16384)].
 Defined.
 
 Definition integer_hash : val := λ: "i", "i" * #654435761.
@@ -182,30 +181,35 @@ Qed.
 
 Instance zero_unit : Unit ZC := 0.
 
-Instance zero_join : Join zero_ord :=
+Program Instance zero_join : Join zero_ord :=
   { join a b := if decide (a = 0) then Some b else if decide (b = 0) then Some a
       else if decide (a = b) then Some a else None }.
-Proof.
-  - constructor; first constructor; repeat intro; unfold zero_ord in *; auto.
-    + destruct H, H0; subst; auto.
-    + destruct H, H0; subst; auto.
-  - constructor; auto.
-  - intros.
-    destruct (decide (a = 0)), (decide (b = 0)); last (destruct (decide (a = b))); inversion H;
-      subst; eauto; destruct (decide (c = 0)); subst; eauto; try done.
-    destruct (decide _); last destruct (decide _); inversion H0; subst; do 2 eexists; eauto;
-      destruct (decide _); auto; rewrite decide_left; auto.
-  - repeat intro.
+Next Obligation.
+  constructor; first constructor; repeat intro; unfold zero_ord in *; auto.
+  - destruct H, H0; subst; auto.
+  - destruct H, H0; subst; auto. Qed.
+Next Obligation. constructor; auto. Qed.
+Next Obligation. intros ???? ?. simpl.
+  destruct (decide (a = 0)), (decide (b = 0)); last (destruct (decide (a = b)));
+    intros H; inversion H;
+    subst; eauto; destruct (decide (c = 0)); subst; eauto; try done.
+  destruct (decide _); last destruct (decide _); intros H0; inversion H0; subst;
+    do 2 eexists; eauto;
+    destruct (decide _); auto; rewrite decide_left; auto. Qed.
+Next Obligation.
+  repeat intro.
     destruct (decide _), (decide _); subst; auto.
-    destruct (decide _), (decide _); subst; auto; done.
-  - intros.
-    unfold zero_ord.
-    destruct (decide _); subst; auto.
-    destruct (decide _); last destruct (decide _); inversion H; auto.
-  - unfold zero_ord; intros; destruct (decide _); auto.
-    destruct H; [contradiction | subst].
-    destruct (decide _); auto.
-    rewrite decide_left; auto.
+    destruct (decide _), (decide _); subst; auto; done. Qed.
+Next Obligation.
+  intros ???. simpl.
+  unfold zero_ord.
+  destruct (decide _); subst; auto.
+  destruct (decide _); last destruct (decide _); intros H; inversion H; auto. Qed.
+Next Obligation.
+  unfold zero_ord; intros; destruct (decide _); auto.
+  destruct H; [contradiction | subst].
+  destruct (decide _); auto.
+  rewrite decide_left; auto.
 Qed.
 
 Section Interpretation.
diff --git a/theories/examples/hist_protocol.v b/theories/examples/hist_protocol.v
index 192f05b4d14edb75769ad191f69a0951871e9236..b3398b9bd27df15252825f6f9abf1daf385af259 100644
--- a/theories/examples/hist_protocol.v
+++ b/theories/examples/hist_protocol.v
@@ -98,34 +98,39 @@ Qed.
 
 End gmaps.
 
-Instance hist_join (A : ofeT) {D : OfeDiscrete A} {L : LeibnizEquiv A} {U : Unit A} `{EqDecision A} : Join
-  (fun (a b : gmapC nat A) => map_subseteq(M := gmap nat)(A := A) a b) :=
+Program Instance hist_join (A : ofeT) {D : OfeDiscrete A} {L : LeibnizEquiv A}
+  {U : Unit A} `{EqDecision A} :
+  Join (fun (a b : gmapC nat A) => map_subseteq(M := gmap nat)(A := A) a b) :=
   { join (m1 m2 : gmapC nat A) := if decide (compatible m1 m2)
       then Some (union m1 m2) else None }.
-Proof.
-  - repeat intro.
-    rewrite lookup_empty; destruct (a !! i) eqn: Ha; rewrite Ha; done.
-  - intros ?????; destruct (decide _); last discriminate.
-    destruct (decide _); last discriminate.
-    intros Ha Hb; inversion Ha; inversion Hb; subst.
-    exists (a ∪ d).
-    destruct (decide _).
-    split; auto.
-    assert (compatible b a) by (rewrite comm; done).
-    destruct (decide _).
-    rewrite fin_maps.Assoc_instance_0 (compatible_union_comm b a); auto.
-    { contradiction n; apply compatible_union_assoc; auto.
-      rewrite compatible_union_comm; auto. }
-    { contradiction n.
-      eapply compatible_subset; eauto.
-      apply (map_union_subseteq_l a b). }
-  - repeat intro.
-    destruct (decide _), (decide _); auto; first (rewrite compatible_union_comm; auto);
-      contradiction n; rewrite compatible_comm; auto.
-  - intros.
-    destruct (decide _); inversion H; subst.
-    apply (map_union_subseteq_l a b).
-  - intros.
-    destruct (decide _); [|contradiction n; apply subset_compatible; auto].
-    apply f_equal, (map_subseteq_union a b); auto.
-Qed.
+Next Obligation.
+  repeat intro.
+  rewrite lookup_empty; destruct (a !! i) eqn: Ha; rewrite Ha; done. Qed.
+Next Obligation.
+  intros ??????????. simpl.
+  destruct (decide _); last discriminate.
+  destruct (decide _); last discriminate.
+  intros Ha Hb; inversion Ha; inversion Hb; subst.
+  exists (a ∪ d).
+  destruct (decide _).
+  split; auto.
+  assert (compatible b a) by (rewrite comm; done).
+  destruct (decide _).
+  rewrite fin_maps.Assoc_instance_0 (compatible_union_comm b a); auto.
+  { contradiction n; apply compatible_union_assoc; auto.
+    rewrite compatible_union_comm; auto. }
+  { contradiction n.
+    eapply compatible_subset; eauto.
+    apply (map_union_subseteq_l a b). } Qed.
+Next Obligation.
+  repeat intro.
+  destruct (decide _), (decide _); auto; first (rewrite compatible_union_comm; auto);
+    contradiction n; rewrite compatible_comm; auto. Qed.
+Next Obligation.
+  intros ????????. simpl.
+  destruct (decide _); intros H; inversion H; subst.
+  apply (map_union_subseteq_l a b). Qed.
+Next Obligation.
+  intros. simpl.
+  destruct (decide _); [|contradiction n; apply subset_compatible; auto].
+  apply f_equal, (map_subseteq_union a b); auto. Qed.
diff --git a/theories/examples/kvnode.v b/theories/examples/kvnode.v
index 30b54b70f3ef6acc1a9d3d8935df679c3f26186a..251dd9037f54170e82655d119ef260211a8f6b75 100644
--- a/theories/examples/kvnode.v
+++ b/theories/examples/kvnode.v
@@ -31,7 +31,6 @@ Program Definition read : val := @RecV <> "n" (λ: "out",
           let: "v" := ["n" + #version]_at in
           if: "v" = "snap" then #() else "f" #()) #()) _.
 Next Obligation.
-Proof.
   apply I.
 Qed.
 
@@ -42,7 +41,6 @@ Program Definition write : val := @RecV <> "n" (λ: "in",
           ["n" + #data + "i"]_at <- ["in" + "i"]_na);;
   ["n" + #version]_at <- ("v" + #2)) _.
 Next Obligation.
-Proof.
   apply I.
 Qed.
 
@@ -53,7 +51,6 @@ Program Definition make_node : val := @RecV <> <>
         ["n" + #data + "i"]_na <- #0);;
    "n") _.
 Next Obligation.
-Proof.
   apply I.
 Qed.
 
@@ -82,19 +79,15 @@ Instance versionPrt_facts : protocol_facts versionProtocol.
 Proof. esplit; apply _.
 Qed.
 
-Instance version_join : Join le := { join a b := Some (max a b) }.
-Proof.
-  - apply Nat.le_0_l.
-  - intros ????? Hc He; inversion Hc; inversion He; subst.
-    do 2 eexists; eauto.
-    by rewrite Max.max_assoc (Max.max_comm a b).
-  - intros ??.
-    by rewrite Max.max_comm.
-  - intros ??? X; inversion X.
-    apply Nat.le_max_l.
-  - intros.
-    by rewrite Max.max_r.
-Qed.
+Program Instance version_join : Join le := { join a b := Some (max a b) }.
+Next Obligation. apply Nat.le_0_l. Qed.
+Next Obligation.
+  intros ????? Hc He; inversion Hc; inversion He; subst.
+  do 2 eexists; eauto.
+  by rewrite Max.max_assoc (Max.max_comm a b). Qed.
+Next Obligation. intros ??. by rewrite Max.max_comm. Qed.
+Next Obligation. intros ??? X; inversion X. apply Nat.le_max_l. Qed.
+Next Obligation. intros. simpl. by rewrite Max.max_r. Qed.
 
 Definition log_latest {A} (m : gmap nat A) n v := m !! n = Some v /\
   forall n', is_Some (m !! n') <-> even n' = true /\ (n' <= n)%nat.
diff --git a/theories/examples/rcu_data.v b/theories/examples/rcu_data.v
index 290c9bfa2d2c2da5912554dd5c5f0b6537834cd7..071c36c3dd397322a9e77b3ed959931c2d377eac 100644
--- a/theories/examples/rcu_data.v
+++ b/theories/examples/rcu_data.v
@@ -30,9 +30,8 @@ Section RCUData.
   Proof. intros [] []; naive_solver. Qed.
 
   Global Instance AbsLoc_eqdec : EqDecision AbsLoc := inj_eq_dec AbsLoc_to_sum.
-  Global Instance AbsLoc_countable: Countable AbsLoc
-    := inj_countable AbsLoc_to_sum (Some ∘ sum_to_AbsLoc) _.
-  Proof. by destruct 0. Qed.
+  Global Instance AbsLoc_countable: Countable AbsLoc.
+  Proof. refine (inj_countable AbsLoc_to_sum (Some ∘ sum_to_AbsLoc) _); by intros []. Qed.
 
   Definition RCUInfo : Type := list (aloc * loc * gname).
   Definition RCUHist : Type := list (aloc * AbsLoc).
diff --git a/theories/machine.v b/theories/machine.v
index 2e586b18f05b98b09375fd2d8b252aa13fc9a607..79dc5bcf8af9606594ea5d769e51978e223acba4 100644
--- a/theories/machine.v
+++ b/theories/machine.v
@@ -241,7 +241,7 @@ Section RAMachine.
           _ : pairwise_disj msgs
         }.
 
-    Definition memory_ok : ∀ M, pairwise_disj M.(msgs) := ltac:(by destruct 0).
+    Definition memory_ok : ∀ M, pairwise_disj M.(msgs) := ltac:(by intros []).
 
     Program Definition add_ins (M : memory) m : MS_msg_disj M m -> memory :=
       fun H => mkMemory (msgs M ∪ {[m]}) _.
@@ -302,7 +302,7 @@ Section RAMachine.
         move => ? ? /elem_of_empty [].
     Qed.
 
-    Global Instance state_Inhabited : Inhabited state := _.
+    Global Instance state_Inhabited : Inhabited state.
     Proof.
       do 2!econstructor; exact: inhabitant.
     Qed.
@@ -938,16 +938,16 @@ Section RAMachine.
               simpl in HAcc; try by (simplify_option_eq; tauto);
                 try (rewrite LT in LV; inversion LV; subst; clear LV);
                 (apply Lt in LT || apply Lt in LV); try by [].
-        - move => m /elem_of_union [|/elem_of_singleton ->] /=;
-            last (by inversion 0);
-            move => In Eq; move : (DInv _ In Eq); intros [[HMax]|];
+        - move => m /elem_of_union [|/elem_of_singleton ->] /= In;
+            last (by inversion In);
+            move => Eq; move : (DInv _ In Eq); intros [[HMax]|];
                     [left|right; exact: dealloc_inv_helper1].
           case: (decide (x0 = mloc m)) => [Eqx0|NEqx0];
             last exact: dealloc_inv_helper2.
           subst. exfalso. eapply max_D_not_allocated => //.
-        - move => m /elem_of_union [|/elem_of_singleton ->] /=;
-            last (by inversion 0);
-            move => In Eq; move : (DInv _ In Eq); intros [[HMax]|];
+        - move => m /elem_of_union [|/elem_of_singleton ->] /= In;
+            last (by inversion In);
+            move => Eq; move : (DInv _ In Eq); intros [[HMax]|];
                     [left|right; exact: dealloc_inv_helper1].
           case: (decide (x0 = mloc m)) => [Eqx0|NEqx0];
             last exact: dealloc_inv_helper2.
diff --git a/theories/na.v b/theories/na.v
index 981e05a020a72d3ed350c117d0b12d240ae10b52..51c8bccefc11ff06fb447931787bfe90893d9edc 100644
--- a/theories/na.v
+++ b/theories/na.v
@@ -63,13 +63,13 @@ Section Exclusive.
     iIntros (?) "[H _] /=". iDestruct "H" as (?) "?". iExists _. eauto.
   Qed.
 
-  Global Instance valloc_local_timeless Σ h : Timeless (@valloc_local Σ h).
+  Global Instance valloc_local_timeless h : Timeless (@valloc_local Σ h).
   Proof.
     rewrite valloc_local_eq /valloc_local_def /= /Timeless. iStartProof (uPred _).
     iIntros (?) "/=". iApply timeless.
   Qed.
 
-  Global Instance valloc_local_Persistent Σ h : Persistent (@valloc_local Σ h).
+  Global Instance valloc_local_Persistent h : Persistent (@valloc_local Σ h).
   Proof.
     rewrite valloc_local_eq /valloc_local_def /= /Persistent. iStartProof (uPred _).
     iIntros (?) "/=". iApply persistent.
diff --git a/theories/types.v b/theories/types.v
index 43bf45da05a7b89e4a22bb96d95c9308ac10f388..a3ea513868067de55579aa405148fad569425e51 100644
--- a/theories/types.v
+++ b/theories/types.v
@@ -39,14 +39,12 @@ Section Definitions.
   Proof. by intros [] [] ?; simplify_eq/=. Qed.
 
   Global Instance Val_dec_eq : EqDecision Val := inj_eq_dec val_to_sum.
-  Global Instance Val_countable : Countable Val :=
-    inj_countable val_to_sum (Some ∘ sum_to_val) _.
-  Proof. by destruct 0. Qed.
+  Global Instance Val_countable : Countable Val.
+  Proof. refine (inj_countable val_to_sum (Some ∘ sum_to_val) _); by intros []. Qed.
 
   Global Instance msg_dec_eq : EqDecision message := inj_eq_dec msg_to_tuple.
-  Global Instance msg_countable : Countable message :=
-    inj_countable msg_to_tuple (Some ∘ tuple_to_msg) _.
-  Proof. by destruct 0. Qed.
+  Global Instance msg_countable : Countable message.
+  Proof. refine (inj_countable msg_to_tuple (Some ∘ tuple_to_msg) _); by intros []. Qed.
 
   Implicit Type (x t : positive) (R V : View) (m : message).
 
@@ -89,9 +87,8 @@ Section Definitions.
     Proof. intros [] []; naive_solver. Qed.
 
     Global Instance access_dec_eq : EqDecision access | 20 := inj_eq_dec acc_to_sum.
-    Global Instance access_countable : Countable access | 20 :=
-      inj_countable acc_to_sum (Some ∘ sum_to_acc) _.
-    Proof. by destruct 0. Qed.
+    Global Instance access_countable : Countable access | 20.
+    Proof. refine (inj_countable acc_to_sum (Some ∘ sum_to_acc) _); by intros []. Qed.
 
   End Glue.