diff --git a/stdpp/countable.v b/stdpp/countable.v
index e24e6111a70f64f33b42736a84688c20163386d9..50c356c56e2c420d171c53593e9c88df37584b2b 100644
--- a/stdpp/countable.v
+++ b/stdpp/countable.v
@@ -61,10 +61,9 @@ Section choice.
     { intros help. by apply (help (encode x)). }
     intros i. induction i as [|i IH] using Pos.peano_ind; intros p ??.
     { constructor. intros j. assert (p = encode x) by lia; subst.
-      inversion 1 as [? Hd|?? Hd]; subst;
-        rewrite decode_encode in Hd; congruence. }
+      inv 1 as [? Hd|?? Hd]; rewrite decode_encode in Hd; congruence. }
     constructor. intros j.
-    inversion 1 as [? Hd|? y Hd]; subst; auto with lia.
+    inv 1 as [? Hd|? y Hd]; auto with lia.
   Qed.
 
   Context `{∀ x, Decision (P x)}.
diff --git a/stdpp/fin_map_dom.v b/stdpp/fin_map_dom.v
index 653a069ece4a92f7d33b7d22c20be02f3463b674..f4e9ee310212cabc8c9931d14cfd955c195e1f17 100644
--- a/stdpp/fin_map_dom.v
+++ b/stdpp/fin_map_dom.v
@@ -49,7 +49,7 @@ Proof. apply not_elem_of_dom. Qed.
 Lemma subseteq_dom {A} (m1 m2 : M A) : m1 ⊆ m2 → dom m1 ⊆ dom m2.
 Proof.
   rewrite map_subseteq_spec.
-  intros ??. rewrite !elem_of_dom. inversion 1; eauto.
+  intros ??. rewrite !elem_of_dom. inv 1; eauto.
 Qed.
 Lemma subset_dom {A} (m1 m2 : M A) : m1 ⊂ m2 → dom m1 ⊂ dom m2.
 Proof.
diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 603fd13ac36cc0af945cb9d84c02b5cb742d8ab2..85eecad3503d32746806fb1aad0dd65ea7882d5e 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -255,7 +255,7 @@ Lemma lookup_weaken {A} (m1 m2 : M A) i x :
 Proof. rewrite !map_subseteq_spec. auto. Qed.
 Lemma lookup_weaken_is_Some {A} (m1 m2 : M A) i :
   is_Some (m1 !! i) → m1 ⊆ m2 → is_Some (m2 !! i).
-Proof. inversion 1. eauto using lookup_weaken. Qed.
+Proof. inv 1. eauto using lookup_weaken. Qed.
 Lemma lookup_weaken_None {A} (m1 m2 : M A) i :
   m2 !! i = None → m1 ⊆ m2 → m1 !! i = None.
 Proof.
@@ -274,7 +274,7 @@ Proof.
   - intros Hm. apply map_eq. intros i. by rewrite Hm, lookup_empty.
 Qed.
 Lemma lookup_empty_is_Some {A} i : ¬is_Some ((∅ : M A) !! i).
-Proof. rewrite lookup_empty. by inversion 1. Qed.
+Proof. rewrite lookup_empty. by inv 1. Qed.
 Lemma lookup_empty_Some {A} i (x : A) : ¬(∅ : M A) !! i = Some x.
 Proof. by rewrite lookup_empty. Qed.
 Lemma lookup_total_empty `{!Inhabited A} i : (∅ : M A) !!! i = inhabitant.
@@ -1213,7 +1213,7 @@ Lemma map_size_list_to_map {A} (l : list (K * A)) :
   NoDup l.*1 →
   size (list_to_map l : M A) = length l.
 Proof.
-  induction l; csimpl; inversion 1; simplify_eq/=; [by rewrite map_size_empty|].
+  induction l; csimpl; inv 1; simplify_eq/=; [by rewrite map_size_empty|].
   rewrite map_size_insert_None by eauto using not_elem_of_list_to_map_1.
   eauto with f_equal.
 Qed.
@@ -3265,7 +3265,7 @@ Section setoid.
     intros i1 x1 i2 x2 Heq. specialize (Heq i1).
     rewrite lookup_singleton in Heq. destruct (decide (i1 = i2)) as [->|].
     - rewrite lookup_singleton in Heq. apply (inj _) in Heq. naive_solver.
-    - rewrite lookup_singleton_ne in Heq by done. inversion Heq.
+    - rewrite lookup_singleton_ne in Heq by done. inv Heq.
   Qed.
 
   Global Instance map_fmap_equiv_inj `{Equiv B} (f : A → B) :
diff --git a/stdpp/lexico.v b/stdpp/lexico.v
index 8f551c113299268aadaa82c9886c0b91be4c250e..e8695ddc993ea816dc5ceaf1a85e654bb61b3d88 100644
--- a/stdpp/lexico.v
+++ b/stdpp/lexico.v
@@ -138,7 +138,7 @@ Proof.
   | _ :: _, [] => inright _
   | x1 :: l1, x2 :: l2 => cast_trichotomy (trichotomyT lexico (x1,l1) (x2,l2))
   end); clear tA go go';
-    abstract (repeat (done || constructor || congruence || by inversion 1)).
+    abstract (repeat (done || constructor || congruence || by inv 1)).
 Defined.
 
 Global Instance sig_lexico_po `{Lexico A, !StrictOrder (@lexico A _)}
diff --git a/stdpp/option.v b/stdpp/option.v
index 796fc546ff182d4820e760e6749f95d834c9a3f3..02e02016164b7daf5dacf534dc090b112b93d82a 100644
--- a/stdpp/option.v
+++ b/stdpp/option.v
@@ -147,7 +147,7 @@ Section setoids.
   Lemma None_equiv_eq mx : mx ≡ None ↔ mx = None.
   Proof. split; [by inv 1|intros ->; constructor]. Qed.
   Lemma Some_equiv_eq mx y : mx ≡ Some y ↔ ∃ y', mx = Some y' ∧ y' ≡ y.
-  Proof. split; [inversion 1; naive_solver|naive_solver (by constructor)]. Qed.
+  Proof. split; [inv 1; naive_solver|naive_solver (by constructor)]. Qed.
 
   Global Instance is_Some_proper : Proper ((≡@{option A}) ==> iff) is_Some.
   Proof. by inv 1. Qed.
@@ -183,7 +183,7 @@ Global Instance option_mfail: MFail option := λ _ _, None.
 
 Lemma option_fmap_inj {A B} (R1 : A → A → Prop) (R2 : B → B → Prop) (f : A → B) :
   Inj R1 R2 f → Inj (option_Forall2 R1) (option_Forall2 R2) (fmap f).
-Proof. intros ? [?|] [?|]; inversion 1; constructor; auto. Qed.
+Proof. intros ? [?|] [?|]; inv 1; constructor; auto. Qed.
 Global Instance option_fmap_eq_inj {A B} (f : A → B) :
   Inj (=) (=) f → Inj (=@{option A}) (=@{option B}) (fmap f).
 Proof.
@@ -247,7 +247,7 @@ Lemma bind_Some {A B} (f : A → option B) (mx : option A) y :
 Proof. destruct mx; naive_solver. Qed.
 Lemma bind_Some_equiv {A} `{Equiv B} (f : A → option B) (mx : option A) y :
   mx ≫= f ≡ Some y ↔ ∃ x, mx = Some x ∧ f x ≡ Some y.
-Proof. destruct mx; (split; [inversion 1|]); naive_solver. Qed.
+Proof. destruct mx; split; first [by inv 1|naive_solver]. Qed.
 Lemma bind_None {A B} (f : A → option B) (mx : option A) :
   mx ≫= f = None ↔ mx = None ∨ ∃ x, mx = Some x ∧ f x = None.
 Proof. destruct mx; naive_solver. Qed.
diff --git a/stdpp/relations.v b/stdpp/relations.v
index 97ed727813974fb9f4c7d8d68fbd1dec4dbc7119..50442d6fab533c8a80f476ebb54bf42b9ba54747 100644
--- a/stdpp/relations.v
+++ b/stdpp/relations.v
@@ -143,7 +143,7 @@ Section general.
   Lemma nsteps_once x y : R x y → nsteps R 1 x y.
   Proof. eauto. Qed.
   Lemma nsteps_once_inv x y : nsteps R 1 x y → R x y.
-  Proof. inversion 1 as [|???? Hhead Htail]; by inv Htail. Qed.
+  Proof. inv 1 as [|???? Hhead Htail]; by inv Htail. Qed.
   Lemma nsteps_trans n m x y z :
     nsteps R n x y → nsteps R m y z → nsteps R (n + m) x z.
   Proof. induction 1; simpl; eauto. Qed.
@@ -354,7 +354,7 @@ Section general.
   Lemma ex_loop_inv x :
     ex_loop R x →
     ∃ x', R x x' ∧ ex_loop R x'.
-  Proof. inversion 1; eauto. Qed.
+  Proof. inv 1; eauto. Qed.
 
 End general.
 
diff --git a/stdpp/sorting.v b/stdpp/sorting.v
index 05a3645b38d1dff148d1b92e37a1610f53fd2663..04308fbd1e03e7e55bcc1b797337036150669201 100644
--- a/stdpp/sorting.v
+++ b/stdpp/sorting.v
@@ -82,7 +82,7 @@ Section sorted.
     { rewrite Forall_forall in Hx1, Hx2.
       assert (x2 ∈ x1 :: l1) as Hx2' by (by rewrite E; left).
       assert (x1 ∈ x2 :: l2) as Hx1' by (by rewrite <-E; left).
-      inversion Hx1'; inversion Hx2'; simplify_eq; auto. }
+      inv Hx1'; inv Hx2'; simplify_eq; auto. }
     f_equal. by apply IH, (inj (x2 ::.)).
   Qed.
   Lemma Sorted_unique `{!Transitive R, !AntiSymm (=) R} l1 l2 :
@@ -96,7 +96,7 @@ Section sorted.
     match l with
     | [] => left _
     | y :: l => cast_if (decide (R x y))
-    end; abstract first [by constructor | by inversion 1].
+    end; abstract first [by constructor | by inv 1].
   Defined.
   Global Instance Sorted_dec `{∀ x y, Decision (R x y)} : ∀ l,
     Decision (Sorted R l).
@@ -106,7 +106,7 @@ Section sorted.
     match l return Decision (Sorted R l) with
     | [] => left _
     | x :: l => cast_if_and (decide (HdRel R x l)) (go l)
-    end); clear go; abstract first [by constructor | by inversion 1].
+    end); clear go; abstract first [by constructor | by inv 1].
   Defined.
   Global Instance StronglySorted_dec `{∀ x y, Decision (R x y)} : ∀ l,
     Decision (StronglySorted R l).
@@ -116,7 +116,7 @@ Section sorted.
     match l return Decision (StronglySorted R l) with
     | [] => left _
     | x :: l => cast_if_and (decide (Forall (R x) l)) (go l)
-    end); clear go; abstract first [by constructor | by inversion 1].
+    end); clear go; abstract first [by constructor | by inv 1].
   Defined.
 
   Section fmap.
@@ -144,9 +144,9 @@ Section sorted.
     induction 1 as [|y l Hsort IH Hhd]; intros Htl; simpl.
     { repeat constructor. }
     constructor.
-    - apply IH. inversion Htl as [|? [|??]]; simplify_list_eq; by constructor.
+    - apply IH. inv Htl as [|? [|??]]; simplify_list_eq; by constructor.
     - destruct Hhd; constructor; [|done].
-      inversion Htl as [|? [|??]]; by try discriminate_list.
+      inv Htl as [|? [|??]]; by try discriminate_list.
   Qed.
 End sorted.