diff --git a/theories/base.v b/theories/base.v
index 56dcd6acf81dc711512bce067aa436c81bdcb015..3570aae7cad56e64c37f66c2f1896dc18ec0e21e 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -5,18 +5,32 @@ that are used throughout the whole development. Most importantly it contains
 abstract interfaces for ordered structures, collections, and various other data
 structures. *)
 Global Generalizable All Variables.
-Global Unset Transparent Obligations.
 From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
 Set Default Proof Using "Type".
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
 
-(* Tweak program: don't let it automatically simplify obligations and hide
-them from the results of the [Search] commands. *)
+(** * Tweak program *)
+(** 1. Since we only use Program to solve logical side-conditions, they should
+always be made Opaque, otherwise we end up with performance problems due to
+Coq blindly unfolding them.
+
+Note that in most cases we use [Next Obligation. (* ... *) Qed.], for which
+this option does not matter. However, sometimes we write things like
+[Solve Obligations with naive_solver (* ... *)], and then the obligations
+should surely be opaque. *)
+Global Unset Transparent Obligations.
+
+(** 2. Do not let Program automatically simplify obligations. The default
+obligation tactic is [Tactics.program_simpl], which, among other things,
+introduces all variables and gives them fresh names. As such, it becomes
+impossible to refer to hypotheses in a robust way. *)
 Obligation Tactic := idtac.
+
+(** 3. Hide obligations from the results of the [Search] commands. *)
 Add Search Blacklist "_obligation_".
 
-(** Sealing off definitions *)
+(** * Sealing off definitions *)
 Section seal.
   Local Set Primitive Projections.
   Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
@@ -24,7 +38,7 @@ End seal.
 Arguments unseal {_ _} _ : assert.
 Arguments seal_eq {_ _} _ : assert.
 
-(** Typeclass opaque definitions *)
+(** * Typeclass opaque definitions *)
 (* The constant [tc_opaque] is used to make definitions opaque for just type
 class search. Note that [simpl] is set up to always unfold [tc_opaque]. *)
 Definition tc_opaque {A} (x : A) : A := x.
@@ -865,23 +879,26 @@ Notation "(≫= f )" := (mbind f) (only parsing) : C_scope.
 Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : C_scope.
 
 Notation "x ← y ; z" := (y ≫= (λ x : _, z))
-  (at level 65, only parsing, right associativity) : C_scope.
+  (at level 100, only parsing, right associativity) : C_scope.
+
 Infix "<$>" := fmap (at level 60, right associativity) : C_scope.
 Notation "' ( x1 , x2 ) ← y ; z" :=
   (y ≫= (λ x : _, let ' (x1, x2) := x in z))
-  (at level 65, only parsing, right associativity) : C_scope.
+  (at level 100, z at level 200, only parsing, right associativity) : C_scope.
 Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
   (y ≫= (λ x : _, let ' (x1,x2,x3) := x in z))
-  (at level 65, only parsing, right associativity) : C_scope.
+  (at level 100, z at level 200, only parsing, right associativity) : C_scope.
 Notation "' ( x1 , x2 , x3  , x4 ) ← y ; z" :=
   (y ≫= (λ x : _, let ' (x1,x2,x3,x4) := x in z))
-  (at level 65, only parsing, right associativity) : C_scope.
+  (at level 100, z at level 200, only parsing, right associativity) : C_scope.
 Notation "' ( x1 , x2 , x3  , x4 , x5 ) ← y ; z" :=
   (y ≫= (λ x : _, let ' (x1,x2,x3,x4,x5) := x in z))
-  (at level 65, only parsing, right associativity) : C_scope.
+  (at level 100, z at level 200, only parsing, right associativity) : C_scope.
 Notation "' ( x1 , x2 , x3  , x4 , x5 , x6 ) ← y ; z" :=
   (y ≫= (λ x : _, let ' (x1,x2,x3,x4,x5,x6) := x in z))
-  (at level 65, only parsing, right associativity) : C_scope.
+  (at level 100, z at level 200, only parsing, right associativity) : C_scope.
+Notation "x ;; z" := (x ≫= λ _, z)
+  (at level 100, z at level 200, only parsing, right associativity): C_scope.
 
 Notation "ps .*1" := (fmap (M:=list) fst ps)
   (at level 10, format "ps .*1").
@@ -891,11 +908,10 @@ Notation "ps .*2" := (fmap (M:=list) snd ps)
 Class MGuard (M : Type → Type) :=
   mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A.
 Arguments mguard _ _ _ !_ _ _ / : assert.
-Notation "'guard' P ; o" := (mguard P (λ _, o))
-  (at level 65, only parsing, right associativity) : C_scope.
-Notation "'guard' P 'as' H ; o" := (mguard P (λ H, o))
-  (at level 65, only parsing, right associativity) : C_scope.
-
+Notation "'guard' P ; z" := (mguard P (λ _, z))
+  (at level 100, z at level 200, only parsing, right associativity) : C_scope.
+Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z))
+  (at level 100, z at level 200, only parsing, right associativity) : C_scope.
 
 (** * Operations on maps *)
 (** In this section we define operational type classes for the operations
diff --git a/theories/collections.v b/theories/collections.v
index 00522a5cd3be4e1bdb9f97e28edd344b04908e3b..5ec1412ea84aa829c4670de9932db164981d0712 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -797,7 +797,7 @@ Global Instance collection_guard `{CollectionMonad M} : MGuard M :=
 Section collection_monad_base.
   Context `{CollectionMonad M}.
   Lemma elem_of_guard `{Decision P} {A} (x : A) (X : M A) :
-    x ∈ guard P; X ↔ P ∧ x ∈ X.
+    (x ∈ guard P; X) ↔ P ∧ x ∈ X.
   Proof.
     unfold mguard, collection_guard; simpl; case_match;
       rewrite ?elem_of_empty; naive_solver.
@@ -805,7 +805,7 @@ Section collection_monad_base.
   Lemma elem_of_guard_2 `{Decision P} {A} (x : A) (X : M A) :
     P → x ∈ X → x ∈ guard P; X.
   Proof. by rewrite elem_of_guard. Qed.
-  Lemma guard_empty `{Decision P} {A} (X : M A) : guard P; X ≡ ∅ ↔ ¬P ∨ X ≡ ∅.
+  Lemma guard_empty `{Decision P} {A} (X : M A) : (guard P; X) ≡ ∅ ↔ ¬P ∨ X ≡ ∅.
   Proof.
     rewrite !elem_of_equiv_empty; setoid_rewrite elem_of_guard.
     destruct (decide P); naive_solver.
@@ -945,7 +945,7 @@ Section collection_monad.
 
   Lemma collection_bind_singleton {A B} (f : A → M B) x : {[ x ]} ≫= f ≡ f x.
   Proof. set_solver. Qed.
-  Lemma collection_guard_True {A} `{Decision P} (X : M A) : P → guard P; X ≡ X.
+  Lemma collection_guard_True {A} `{Decision P} (X : M A) : P → (guard P; X) ≡ X.
   Proof. set_solver. Qed.
   Lemma collection_fmap_compose {A B C} (f : A → B) (g : B → C) (X : M A) :
     g ∘ f <$> X ≡ g <$> (f <$> X).
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 9db4afcb072ec8f06ca0db6f51b0309b0c513bc2..903c17672abb351a30fd7ac467de6f3d11faab3f 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1212,7 +1212,7 @@ End more_merge.
 
 (** Properties of the zip_with function *)
 Lemma map_lookup_zip_with {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i :
-  map_zip_with f m1 m2 !! i = x ← m1 !! i; y ← m2 !! i; Some (f x y).
+  map_zip_with f m1 m2 !! i = (x ← m1 !! i; y ← m2 !! i; Some (f x y)).
 Proof.
   unfold map_zip_with. rewrite lookup_merge by done.
   by destruct (m1 !! i), (m2 !! i).
diff --git a/theories/finite.v b/theories/finite.v
index ab14c0e092bd3098f9486593d00a2fe459fe80b2..a44bfe75385a3f9a890f4b57d4ba8cbdccd08975 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -72,7 +72,7 @@ Definition encode_fin `{Finite A} (x : A) : fin (card A) :=
   Fin.of_nat_lt (encode_lt_card x).
 Program Definition decode_fin `{Finite A} (i : fin (card A)) : A :=
   match Some_dec (decode_nat i) return _ with
-  | inleft (exist _ x _) => x | inright _ => _
+  | inleft (x ↾ _) => x | inright _ => _
   end.
 Next Obligation.
   intros A ?? i ?; exfalso.
diff --git a/theories/hlist.v b/theories/hlist.v
index ae4f934180b429c4ebf93f06a92a3da2ed36ad5f..046a419d7eeeedd814f8298d50eb3e0b2a64d5ec 100644
--- a/theories/hlist.v
+++ b/theories/hlist.v
@@ -40,10 +40,10 @@ Definition hlam {A As B} (f : A → himpl As B) : himpl (tcons A As) B := f.
 Arguments hlam _ _ _ _ _ / : assert.
 
 Definition hcurry {As B} (f : himpl As B) (xs : hlist As) : B :=
-  (fix go As xs :=
+  (fix go {As} xs :=
     match xs in hlist As return himpl As B → B with
     | hnil => λ f, f
-    | @hcons A As x xs => λ f, go As xs (f x)
+    | hcons x xs => λ f, go xs (f x)
     end) _ xs f.
 Coercion hcurry : himpl >-> Funclass.
 
diff --git a/theories/list.v b/theories/list.v
index be077eea5bd39d11782b3e49fd99304ad07510b2..c2cbd8bc9236b217005a3d6c1b588cd43be4a1f4 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3394,7 +3394,7 @@ Section zip_with.
     Forall2 P l k → length (zip_with f l k) = length k.
   Proof. induction 1; simpl; auto. Qed.
   Lemma lookup_zip_with l k i :
-    zip_with f l k !! i = x ← l !! i; y ← k !! i; Some (f x y).
+    zip_with f l k !! i = (x ← l !! i; y ← k !! i; Some (f x y)).
   Proof.
     revert k i. induction l; intros [|??] [|?]; f_equal/=; auto.
     by destruct (_ !! _).
diff --git a/theories/option.v b/theories/option.v
index d50cc7ea0ef185e6e46868c3432186733375665f..f149f442e145c91704392cd27d6fb9500b3d4bdb 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -336,13 +336,13 @@ Tactic Notation "case_option_guard" :=
   let H := fresh in case_option_guard as H.
 
 Lemma option_guard_True {A} P `{Decision P} (mx : option A) :
-  P → guard P; mx = mx.
+  P → (guard P; mx) = mx.
 Proof. intros. by case_option_guard. Qed.
 Lemma option_guard_False {A} P `{Decision P} (mx : option A) :
-  ¬P → guard P; mx = None.
+  ¬P → (guard P; mx) = None.
 Proof. intros. by case_option_guard. Qed.
 Lemma option_guard_iff {A} P Q `{Decision P, Decision Q} (mx : option A) :
-  (P ↔ Q) → guard P; mx = guard Q; mx.
+  (P ↔ Q) → (guard P; mx) = guard Q; mx.
 Proof. intros [??]. repeat case_option_guard; intuition. Qed.
 
 Tactic Notation "simpl_option" "by" tactic3(tac) :=