diff --git a/theories/base.v b/theories/base.v
index c0d9b42814f147279bbccd60828445a70a940e94..323dd30d14e43c84bb6540f63f5ba17ccc7ceb56 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -21,8 +21,8 @@ Add Search Blacklist "_obligation_".
 (** Sealing off definitions *)
 Set Primitive Projections.
 Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
-Arguments unseal {_ _} _.
-Arguments seal_eq {_ _} _.
+Arguments unseal {_ _} _ : assert.
+Arguments seal_eq {_ _} _ : assert.
 Unset Primitive Projections.
 
 (* Below we define type class versions of the common logical operators. It is
@@ -149,13 +149,13 @@ propositions. For example to declare a parameter expressing decidable equality
 on a type [A] we write [`{∀ x y : A, Decision (x = y)}] and use it by writing
 [decide (x = y)]. *)
 Class Decision (P : Prop) := decide : {P} + {¬P}.
-Arguments decide _ {_}.
+Arguments decide _ {_} : assert.
 Notation EqDecision A := (∀ x y : A, Decision (x = y)).
 
 (** ** Inhabited types *)
 (** This type class collects types that are inhabited. *)
 Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
-Arguments populate {_} _.
+Arguments populate {_} _ : assert.
 
 (** ** Proof irrelevant types *)
 (** This type class collects types that are proof irrelevant. That means, all
@@ -198,22 +198,22 @@ Class Trichotomy {A} (R : relation A) :=
 Class TrichotomyT {A} (R : relation A) :=
   trichotomyT x y : {R x y} + {x = y} + {R y x}.
 
-Arguments irreflexivity {_} _ {_} _ _.
-Arguments inj {_ _ _ _} _ {_} _ _ _.
-Arguments inj2 {_ _ _ _ _ _} _ {_} _ _ _ _ _.
-Arguments cancel {_ _ _} _ _ {_} _.
-Arguments surj {_ _ _} _ {_} _.
-Arguments idemp {_ _} _ {_} _.
-Arguments comm {_ _ _} _ {_} _ _.
-Arguments left_id {_ _} _ _ {_} _.
-Arguments right_id {_ _} _ _ {_} _.
-Arguments assoc {_ _} _ {_} _ _ _.
-Arguments left_absorb {_ _} _ _ {_} _.
-Arguments right_absorb {_ _} _ _ {_} _.
-Arguments anti_symm {_ _} _ {_} _ _ _ _.
-Arguments total {_} _ {_} _ _.
-Arguments trichotomy {_} _ {_} _ _.
-Arguments trichotomyT {_} _ {_} _ _.
+Arguments irreflexivity {_} _ {_} _ _ : assert.
+Arguments inj {_ _ _ _} _ {_} _ _ _ : assert.
+Arguments inj2 {_ _ _ _ _ _} _ {_} _ _ _ _ _: assert.
+Arguments cancel {_ _ _} _ _ {_} _ : assert.
+Arguments surj {_ _ _} _ {_} _ : assert.
+Arguments idemp {_ _} _ {_} _ : assert.
+Arguments comm {_ _ _} _ {_} _ _ : assert.
+Arguments left_id {_ _} _ _ {_} _ : assert.
+Arguments right_id {_ _} _ _ {_} _ : assert.
+Arguments assoc {_ _} _ {_} _ _ _ : assert.
+Arguments left_absorb {_ _} _ _ {_} _ : assert.
+Arguments right_absorb {_ _} _ _ {_} _ : assert.
+Arguments anti_symm {_ _} _ {_} _ _ _ _ : assert.
+Arguments total {_} _ {_} _ _ : assert.
+Arguments trichotomy {_} _ {_} _ _ : assert.
+Arguments trichotomyT {_} _ {_} _ _ : assert.
 
 Lemma not_symmetry `{R : relation A, !Symmetric R} x y : ¬R x y → ¬R y x.
 Proof. intuition. Qed.
@@ -371,10 +371,10 @@ Instance impl_inhabited {A} `{Inhabited B} : Inhabited (A → B) :=
 
 (** Ensure that [simpl] unfolds [id], [compose], and [flip] when fully
 applied. *)
-Arguments id _ _ /.
-Arguments compose _ _ _ _ _ _ /.
-Arguments flip _ _ _ _ _ _ /.
-Arguments const _ _ _ _ /.
+Arguments id _ _ / : assert.
+Arguments compose _ _ _ _ _ _ / : assert.
+Arguments flip _ _ _ _ _ _ / : assert.
+Arguments const _ _ _ _ / : assert.
 Typeclasses Transparent id compose flip const.
 
 Definition fun_map {A A' B B'} (f: A' → A) (g: B → B') (h : A → B) : A' → B' :=
@@ -476,11 +476,11 @@ Definition curry4 {A B C D E} (f : A → B → C → D → E) (p : A * B * C * D
 
 Definition prod_map {A A' B B'} (f: A → A') (g: B → B') (p : A * B) : A' * B' :=
   (f (p.1), g (p.2)).
-Arguments prod_map {_ _ _ _} _ _ !_ /.
+Arguments prod_map {_ _ _ _} _ _ !_ / : assert.
 
 Definition prod_zip {A A' A'' B B' B''} (f : A → A' → A'') (g : B → B' → B'')
     (p : A * B) (q : A' * B') : A'' * B'' := (f (p.1) (q.1), g (p.2) (q.2)).
-Arguments prod_zip {_ _ _ _ _ _} _ _ !_ !_ /.
+Arguments prod_zip {_ _ _ _ _ _} _ _ !_ !_ / : assert.
 
 Instance prod_inhabited {A B} (iA : Inhabited A)
     (iB : Inhabited B) : Inhabited (A * B) :=
@@ -536,7 +536,7 @@ Proof. intros [??] [??] [??]; f_equal; apply leibniz_equiv; auto. Qed.
 (** ** Sums *)
 Definition sum_map {A A' B B'} (f: A → A') (g: B → B') (xy : A + B) : A' + B' :=
   match xy with inl x => inl (f x) | inr y => inr (g y) end.
-Arguments sum_map {_ _ _ _} _ _ !_ /.
+Arguments sum_map {_ _ _ _} _ _ !_ / : assert.
 
 Instance sum_inhabited_l {A B} (iA : Inhabited A) : Inhabited (A + B) :=
   match iA with populate x => populate (inl x) end.
@@ -592,13 +592,13 @@ Typeclasses Opaque sum_equiv.
 Instance option_inhabited {A} : Inhabited (option A) := populate None.
 
 (** ** Sigma types *)
-Arguments existT {_ _} _ _.
-Arguments projT1 {_ _} _.
-Arguments projT2 {_ _} _.
+Arguments existT {_ _} _ _ : assert.
+Arguments projT1 {_ _} _ : assert.
+Arguments projT2 {_ _} _ : assert.
 
-Arguments exist {_} _ _ _.
-Arguments proj1_sig {_ _} _.
-Arguments proj2_sig {_ _} _.
+Arguments exist {_} _ _ _ : assert.
+Arguments proj1_sig {_ _} _ : assert.
+Arguments proj2_sig {_ _} _ : assert.
 Notation "x ↾ p" := (exist _ x p) (at level 20) : C_scope.
 Notation "` x" := (proj1_sig x) (at level 10, format "` x") : C_scope.
 
@@ -616,7 +616,7 @@ Section sig_map.
     apply (inj f) in Hxy; subst. rewrite (proof_irrel _ Hy). auto.
   Qed.
 End sig_map.
-Arguments sig_map _ _ _ _ _ _ !_ /.
+Arguments sig_map _ _ _ _ _ _ !_ / : assert.
 
 
 (** * Operations on collections *)
@@ -646,7 +646,7 @@ Infix "∪*∪**" := (zip_with (prod_zip (∪) (∪*)))
   (at level 50, left associativity) : C_scope.
 
 Definition union_list `{Empty A} `{Union A} : list A → A := fold_right (∪) ∅.
-Arguments union_list _ _ _ !_ /.
+Arguments union_list _ _ _ !_ / : assert.
 Notation "⋃ l" := (union_list l) (at level 20, format "⋃  l") : C_scope.
 
 Class Intersection A := intersection: A → A → A.
@@ -792,19 +792,19 @@ and fmap. We use these type classes merely for convenient overloading of
 notations and do not formalize any theory on monads (we do not even define a
 class with the monad laws). *)
 Class MRet (M : Type → Type) := mret: ∀ {A}, A → M A.
-Arguments mret {_ _ _} _.
+Arguments mret {_ _ _} _ : assert.
 Instance: Params (@mret) 3.
 Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B.
-Arguments mbind {_ _ _ _} _ !_ /.
+Arguments mbind {_ _ _ _} _ !_ / : assert.
 Instance: Params (@mbind) 4.
 Class MJoin (M : Type → Type) := mjoin: ∀ {A}, M (M A) → M A.
-Arguments mjoin {_ _ _} !_ /.
+Arguments mjoin {_ _ _} !_ / : assert.
 Instance: Params (@mjoin) 3.
 Class FMap (M : Type → Type) := fmap : ∀ {A B}, (A → B) → M A → M B.
-Arguments fmap {_ _ _ _} _ !_ /.
+Arguments fmap {_ _ _ _} _ !_ / : assert.
 Instance: Params (@fmap) 4.
 Class OMap (M : Type → Type) := omap: ∀ {A B}, (A → option B) → M A → M B.
-Arguments omap {_ _ _ _} _ !_ /.
+Arguments omap {_ _ _ _} _ !_ / : assert.
 Instance: Params (@omap) 4.
 
 Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : C_scope.
@@ -838,7 +838,7 @@ 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 _ _ _ !_ _ _ /.
+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))
@@ -855,7 +855,7 @@ Notation "m !! i" := (lookup i m) (at level 20) : C_scope.
 Notation "(!!)" := lookup (only parsing) : C_scope.
 Notation "( m !!)" := (λ i, m !! i) (only parsing) : C_scope.
 Notation "(!! i )" := (lookup i) (only parsing) : C_scope.
-Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch.
+Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The singleton map *)
 Class SingletonM K A M := singletonM: K → A → M.
@@ -868,20 +868,20 @@ Class Insert (K A M : Type) := insert: K → A → M → M.
 Instance: Params (@insert) 5.
 Notation "<[ k := a ]>" := (insert k a)
   (at level 5, right associativity, format "<[ k := a ]>") : C_scope.
-Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch.
+Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
 
 (** The function delete [delete k m] should delete the value at key [k] in
 [m]. If the key [k] is not a member of [m], the original map should be
 returned. *)
 Class Delete (K M : Type) := delete: K → M → M.
 Instance: Params (@delete) 4.
-Arguments delete _ _ _ !_ !_ / : simpl nomatch.
+Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [alter f k m] should update the value at key [k] using the
 function [f], which is called with the original value. *)
 Class Alter (K A M : Type) := alter: (A → A) → K → M → M.
 Instance: Params (@alter) 5.
-Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch.
+Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [alter f k m] should update the value at key [k] using the
 function [f], which is called with the original value at key [k] or [None]
@@ -890,21 +890,21 @@ yields [None]. *)
 Class PartialAlter (K A M : Type) :=
   partial_alter: (option A → option A) → K → M → M.
 Instance: Params (@partial_alter) 4.
-Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch.
+Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [dom C m] should yield the domain of [m]. That is a finite
 collection of type [C] that contains the keys that are a member of [m]. *)
 Class Dom (M C : Type) := dom: M → C.
 Instance: Params (@dom) 3.
-Arguments dom _ _ _ _ : clear implicits.
-Arguments dom {_} _ {_} !_ / : simpl nomatch.
+Arguments dom : clear implicits.
+Arguments dom {_} _ {_} !_ / : simpl nomatch, assert.
 
 (** The function [merge f m1 m2] should merge the maps [m1] and [m2] by
 constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*)
 Class Merge (M : Type → Type) :=
   merge: ∀ {A B C}, (option A → option B → option C) → M A → M B → M C.
 Instance: Params (@merge) 4.
-Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch.
+Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [union_with f m1 m2] is supposed to yield the union of [m1]
 and [m2] using the function [f] to combine values of members that are in
@@ -912,35 +912,35 @@ both [m1] and [m2]. *)
 Class UnionWith (A M : Type) :=
   union_with: (A → A → option A) → M → M → M.
 Instance: Params (@union_with) 3.
-Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch.
+Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 (** Similarly for intersection and difference. *)
 Class IntersectionWith (A M : Type) :=
   intersection_with: (A → A → option A) → M → M → M.
 Instance: Params (@intersection_with) 3.
-Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch.
+Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 Class DifferenceWith (A M : Type) :=
   difference_with: (A → A → option A) → M → M → M.
 Instance: Params (@difference_with) 3.
-Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch.
+Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 Definition intersection_with_list `{IntersectionWith A M}
   (f : A → A → option A) : M → list M → M := fold_right (intersection_with f).
-Arguments intersection_with_list _ _ _ _ _ !_ /.
+Arguments intersection_with_list _ _ _ _ _ !_ / : assert.
 
 Class LookupE (E K A M : Type) := lookupE: E → K → M → option A.
 Instance: Params (@lookupE) 6.
 Notation "m !!{ Γ } i" := (lookupE Γ i m)
   (at level 20, format "m  !!{ Γ }  i") : C_scope.
 Notation "(!!{ Γ } )" := (lookupE Γ) (only parsing, Γ at level 1) : C_scope.
-Arguments lookupE _ _ _ _ _ _ !_ !_ / : simpl nomatch.
+Arguments lookupE _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 Class InsertE (E K A M : Type) := insertE: E → K → A → M → M.
 Instance: Params (@insertE) 6.
 Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
   (at level 5, right associativity, format "<[ k := a ]{ Γ }>") : C_scope.
-Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch.
+Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
 
 
 (** * Axiomatization of collections *)
@@ -998,7 +998,7 @@ Class FinCollection A C `{ElemOf A C, Empty C, Singleton A C, Union C,
   NoDup_elements X : NoDup (elements X)
 }.
 Class Size C := size: C → nat.
-Arguments size {_ _} !_ / : simpl nomatch.
+Arguments size {_ _} !_ / : simpl nomatch, assert.
 Instance: Params (@size) 2.
 
 (** The class [Collection M] axiomatizes a type constructor [M] that can be
diff --git a/theories/bset.v b/theories/bset.v
index eedd1466e7460cbdcd4b787030edbd238404c005..f3f0d828c0d9e5b1c4d9c0055689d519c81e7166 100644
--- a/theories/bset.v
+++ b/theories/bset.v
@@ -5,8 +5,9 @@ From stdpp Require Export prelude.
 Set Default Proof Using "Type".
 
 Record bset (A : Type) : Type := mkBSet { bset_car : A → bool }.
-Arguments mkBSet {_} _.
-Arguments bset_car {_} _ _.
+Arguments mkBSet {_} _ : assert.
+Arguments bset_car {_} _ _ : assert.
+
 Instance bset_top {A} : Top (bset A) := mkBSet (λ _, true).
 Instance bset_empty {A} : Empty (bset A) := mkBSet (λ _, false).
 Instance bset_singleton `{EqDecision A} : Singleton A (bset A) := λ x,
diff --git a/theories/coPset.v b/theories/coPset.v
index f0bdf92930c8183115200fe14439deda9c452b9f..68b8466fea08fbbc555e05fac3fd95339e275e7e 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -30,7 +30,7 @@ Fixpoint coPset_wf (t : coPset_raw) : bool :=
   | coPNode false (coPLeaf false) (coPLeaf false) => false
   | coPNode b l r => coPset_wf l && coPset_wf r
   end.
-Arguments coPset_wf !_ / : simpl nomatch.
+Arguments coPset_wf !_ / : simpl nomatch, assert.
 
 Lemma coPNode_wf_l b l r : coPset_wf (coPNode b l r) → coPset_wf l.
 Proof. destruct b, l as [[]|],r as [[]|]; simpl; rewrite ?andb_True; tauto. Qed.
@@ -44,7 +44,7 @@ Definition coPNode' (b : bool) (l r : coPset_raw) : coPset_raw :=
   | false, coPLeaf false, coPLeaf false => coPLeaf false
   | _, _, _ => coPNode b l r
   end.
-Arguments coPNode' _ _ _ : simpl never.
+Arguments coPNode' : simpl never.
 Lemma coPNode_wf b l r : coPset_wf l → coPset_wf r → coPset_wf (coPNode' b l r).
 Proof. destruct b, l as [[]|], r as [[]|]; simpl; auto. Qed.
 Hint Resolve coPNode_wf.
@@ -57,7 +57,7 @@ Fixpoint coPset_elem_of_raw (p : positive) (t : coPset_raw) {struct t} : bool :=
   | coPNode _ _ r, p~1 => coPset_elem_of_raw p r
   end.
 Local Notation e_of := coPset_elem_of_raw.
-Arguments coPset_elem_of_raw _ !_ / : simpl nomatch.
+Arguments coPset_elem_of_raw _ !_ / : simpl nomatch, assert.
 Lemma coPset_elem_of_node b l r p :
   e_of p (coPNode' b l r) = e_of p (coPNode b l r).
 Proof. by destruct p, b, l as [[]|], r as [[]|]. Qed.
@@ -99,7 +99,7 @@ Instance coPset_union_raw : Union coPset_raw :=
   | coPLeaf false, coPNode b l r => coPNode b l r
   | coPNode b1 l1 r1, coPNode b2 l2 r2 => coPNode' (b1||b2) (l1 ∪ l2) (r1 ∪ r2)
   end.
-Local Arguments union _ _!_ !_ /.
+Local Arguments union _ _!_ !_ / : assert.
 Instance coPset_intersection_raw : Intersection coPset_raw :=
   fix go t1 t2 := let _ : Intersection _ := @go in
   match t1, t2 with
@@ -110,7 +110,7 @@ Instance coPset_intersection_raw : Intersection coPset_raw :=
   | coPLeaf true, coPNode b l r => coPNode b l r
   | coPNode b1 l1 r1, coPNode b2 l2 r2 => coPNode' (b1&&b2) (l1 ∩ l2) (r1 ∩ r2)
   end.
-Local Arguments intersection _ _!_ !_ /.
+Local Arguments intersection _ _!_ !_ / : assert.
 Fixpoint coPset_opp_raw (t : coPset_raw) : coPset_raw :=
   match t with
   | coPLeaf b => coPLeaf (negb b)
diff --git a/theories/collections.v b/theories/collections.v
index 37ce45f2a979c6bdafb1ba35c581f3ff602165ab..bb6c4b5fcaff5d76ffc8deb361b0922ac5b6a773 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -92,7 +92,7 @@ This transformation is implemented using type classes instead of setoid
 rewriting to ensure that we traverse each term at most once and to be able to
 deal with occurences of the set operations under binders. *)
 Class SetUnfold (P Q : Prop) := { set_unfold : P ↔ Q }.
-Arguments set_unfold _ _ {_}.
+Arguments set_unfold _ _ {_} : assert.
 Hint Mode SetUnfold + - : typeclass_instances.
 
 Class SetUnfoldSimpl (P Q : Prop) := { set_unfold_simpl : SetUnfold P Q }.
diff --git a/theories/fin.v b/theories/fin.v
index 888825cbb92b23d5c8f5b112143796df31b1e85d..4b8cdd0af0de086b221f26f116e68f99bf9f6846 100644
--- a/theories/fin.v
+++ b/theories/fin.v
@@ -18,7 +18,7 @@ Notation fin := Fin.t.
 Notation FS := Fin.FS.
 
 Delimit Scope fin_scope with fin.
-Arguments Fin.FS _ _%fin.
+Arguments Fin.FS _ _%fin : assert.
 
 Notation "0" := Fin.F1 : fin_scope. Notation "1" := (FS 0) : fin_scope.
 Notation "2" := (FS 1) : fin_scope. Notation "3" := (FS 2) : fin_scope.
diff --git a/theories/finite.v b/theories/finite.v
index b68fc61921f6231fda99173d90d59daddef2f472..0a1dff9cda070037e8471693945b9a2d3c8da014 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -8,17 +8,17 @@ Class Finite A `{EqDecision A} := {
   NoDup_enum : NoDup enum;
   elem_of_enum x : x ∈ enum
 }.
-Arguments enum _ _ _ : clear implicits.
-Arguments enum _ {_ _}.
-Arguments NoDup_enum _ _ _ : clear implicits.
-Arguments NoDup_enum _ {_ _}.
+Arguments enum : clear implicits.
+Arguments enum _ {_ _} : assert.
+Arguments NoDup_enum : clear implicits.
+Arguments NoDup_enum _ {_ _} : assert.
 Definition card A `{Finite A} := length (enum A).
 Program Instance finite_countable `{Finite A} : Countable A := {|
   encode := λ x,
     Pos.of_nat $ S $ from_option id 0 $ fst <$> list_find (x =) (enum A);
   decode := λ p, enum A !! pred (Pos.to_nat p)
 |}.
-Arguments Pos.of_nat _ : simpl never.
+Arguments Pos.of_nat : simpl never.
 Next Obligation.
   intros ?? [xs Hxs HA] x; unfold encode, decode; simpl.
   destruct (list_find_elem_of (x =) xs x) as [[i y] Hi]; auto.
diff --git a/theories/gmap.v b/theories/gmap.v
index 4572c9050fd2e3bf85f137d37cf7b9715c7f9745..fe7ddf772f5a9a8590c9210a543d6064d110f154 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -15,8 +15,8 @@ Record gmap K `{Countable K} A := GMap {
   gmap_car : Pmap A;
   gmap_prf : bool_decide (gmap_wf gmap_car)
 }.
-Arguments GMap {_ _ _ _} _ _.
-Arguments gmap_car {_ _ _ _} _.
+Arguments GMap {_ _ _ _} _ _ : assert.
+Arguments gmap_car {_ _ _ _} _ : assert.
 Lemma gmap_eq `{Countable K} {A} (m1 m2 : gmap K A) :
   m1 = m2 ↔ gmap_car m1 = gmap_car m2.
 Proof.
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 0104004366edde950179d4f3471d398729abe80c..084dfdca5b609518591529f7fa862744c284cdec 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -4,8 +4,8 @@ From stdpp Require Import gmap.
 Set Default Proof Using "Type".
 
 Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A nat }.
-Arguments GMultiSet {_ _ _} _.
-Arguments gmultiset_car {_ _ _} _.
+Arguments GMultiSet {_ _ _} _ : assert.
+Arguments gmultiset_car {_ _ _} _ : assert.
 
 Lemma gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A).
 Proof. solve_decision. Defined.
diff --git a/theories/hashset.v b/theories/hashset.v
index b84c1f0849c50d250ac43beac8320bfdd4f26946..59c5506ba5c5527585b551223a16c46cb5f8029c 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -12,8 +12,8 @@ Record hashset {A} (hash : A → Z) := Hashset {
   hashset_prf :
     map_Forall (λ n l, Forall (λ x, hash x = n) l ∧ NoDup l) hashset_car
 }.
-Arguments Hashset {_ _} _ _.
-Arguments hashset_car {_ _} _.
+Arguments Hashset {_ _} _ _ : assert.
+Arguments hashset_car {_ _} _ : assert.
 
 Section hashset.
 Context `{EqDecision A} (hash : A → Z).
diff --git a/theories/hlist.v b/theories/hlist.v
index e36296e60cbd24c02277b91056e08ee3497ede13..90a9830fe3cbb4e6e10fa73a680a41991a0efc65 100644
--- a/theories/hlist.v
+++ b/theories/hlist.v
@@ -37,7 +37,7 @@ Fixpoint himpl (As : tlist) (B : Type) : Type :=
 
 Definition hinit {B} (y : B) : himpl tnil B := y.
 Definition hlam {A As B} (f : A → himpl As B) : himpl (tcons A As) B := f.
-Arguments hlam _ _ _ _ _/.
+Arguments hlam _ _ _ _ _ / : assert.
 
 Definition hcurry {As B} (f : himpl As B) (xs : hlist As) : B :=
   (fix go As xs :=
diff --git a/theories/list.v b/theories/list.v
index 943ef18229dbbf7bcb5e84b520ad9f1e02fd6dc2..5f3bf7840e3ac26ab2cba52be7be27b8e0a30fc1 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -6,9 +6,9 @@ From Coq Require Export Permutation.
 From stdpp Require Export numbers base option.
 Set Default Proof Using "Type*".
 
-Arguments length {_} _.
-Arguments cons {_} _ _.
-Arguments app {_} _ _.
+Arguments length {_} _ : assert.
+Arguments cons {_} _ _ : assert.
+Arguments app {_} _ _ : assert.
 
 Instance: Params (@length) 1.
 Instance: Params (@cons) 1.
@@ -18,16 +18,16 @@ Notation tail := tl.
 Notation take := firstn.
 Notation drop := skipn.
 
-Arguments tail {_} _.
-Arguments take {_} !_ !_ /.
-Arguments drop {_} !_ !_ /.
+Arguments tail {_} _ : assert.
+Arguments take {_} !_ !_ / : assert.
+Arguments drop {_} !_ !_ / : assert.
 
 Instance: Params (@tail) 1.
 Instance: Params (@take) 1.
 Instance: Params (@drop) 1.
 
-Arguments Permutation {_} _ _.
-Arguments Forall_cons {_} _ _ _ _ _.
+Arguments Permutation {_} _ _ : assert.
+Arguments Forall_cons {_} _ _ _ _ _ : assert.
 Remove Hints Permutation_cons : typeclass_instances.
 
 Notation "(::)" := cons (only parsing) : C_scope.
@@ -148,7 +148,7 @@ Fixpoint resize {A} (n : nat) (y : A) (l : list A) : list A :=
   | [] => replicate n y
   | x :: l => match n with 0 => [] | S n => x :: resize n y l end
   end.
-Arguments resize {_} !_ _ !_.
+Arguments resize {_} !_ _ !_ : assert.
 Instance: Params (@resize) 2.
 
 (** The function [reshape k l] transforms [l] into a list of lists whose sizes
@@ -217,8 +217,8 @@ Inductive zipped_Forall {A} (P : list A → list A → A → Prop) :
   | zipped_Forall_nil l : zipped_Forall P l []
   | zipped_Forall_cons l k x :
      P l k x → zipped_Forall P (x :: l) k → zipped_Forall P l (x :: k).
-Arguments zipped_Forall_nil {_ _} _.
-Arguments zipped_Forall_cons {_ _} _ _ _ _ _.
+Arguments zipped_Forall_nil {_ _} _ : assert.
+Arguments zipped_Forall_cons {_ _} _ _ _ _ _ : assert.
 
 (** The function [mask f βs l] applies the function [f] to elements in [l] at
 positions that are [true] in [βs]. *)
@@ -3504,9 +3504,9 @@ over the type of constants, but later we use [nat]s and a list representing
 a corresponding environment. *)
 Inductive rlist (A : Type) :=
   rnil : rlist A | rnode : A → rlist A | rapp : rlist A → rlist A → rlist A.
-Arguments rnil {_}.
-Arguments rnode {_} _.
-Arguments rapp {_} _ _.
+Arguments rnil {_} : assert.
+Arguments rnode {_} _ : assert.
+Arguments rapp {_} _ _ : assert.
 
 Module rlist.
 Fixpoint to_list {A} (t : rlist A) : list A :=
diff --git a/theories/listset.v b/theories/listset.v
index f143e66dc0a9cdb56527b10729e0582786a53701..4649ede5db3ee1661003324e158d57c2c02ec115 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -6,8 +6,8 @@ From stdpp Require Export collections list.
 Set Default Proof Using "Type".
 
 Record listset A := Listset { listset_car: list A }.
-Arguments listset_car {_} _.
-Arguments Listset {_} _.
+Arguments listset_car {_} _ : assert.
+Arguments Listset {_} _ : assert.
 
 Section listset.
 Context {A : Type}.
diff --git a/theories/listset_nodup.v b/theories/listset_nodup.v
index edffa54d329f3465aed4170b5358f4dd251946fe..dbfb2d62ad28b5937f4bfe22e98aaeb5cb51a8ca 100644
--- a/theories/listset_nodup.v
+++ b/theories/listset_nodup.v
@@ -9,9 +9,9 @@ Set Default Proof Using "Type".
 Record listset_nodup A := ListsetNoDup {
   listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car
 }.
-Arguments ListsetNoDup {_} _ _.
-Arguments listset_nodup_car {_} _.
-Arguments listset_nodup_prf {_} _.
+Arguments ListsetNoDup {_} _ _ : assert.
+Arguments listset_nodup_car {_} _ : assert.
+Arguments listset_nodup_prf {_} _ : assert.
 
 Section list_collection.
 Context `{EqDecision A}.
diff --git a/theories/mapset.v b/theories/mapset.v
index 193ab9a956ff39b9658de81fe084ae144a2d31f2..bb44b6711ea679d48c9dc2828cb7253a11615167 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -8,8 +8,8 @@ From stdpp Require Export fin_map_dom.
 
 Record mapset (M : Type → Type) : Type :=
   Mapset { mapset_car: M (unit : Type) }.
-Arguments Mapset {_} _.
-Arguments mapset_car {_} _.
+Arguments Mapset {_} _ : assert.
+Arguments mapset_car {_} _ : assert.
 
 Section mapset.
 Context `{FinMap K M}.
@@ -143,4 +143,5 @@ Hint Extern 1 (Difference (mapset _)) =>
   eapply @mapset_difference : typeclass_instances.
 Hint Extern 1 (Elements _ (mapset _)) =>
   eapply @mapset_elems : typeclass_instances.
-Arguments mapset_eq_dec _ _ _ _ : simpl never.
+
+Arguments mapset_eq_dec : simpl never.
diff --git a/theories/natmap.v b/theories/natmap.v
index 87802090a433de71a362bad132317b8eb5799ad6..daa00e46668006913c7e85fc8e0961c902af089b 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -28,9 +28,9 @@ Record natmap (A : Type) : Type := NatMap {
   natmap_car : natmap_raw A;
   natmap_prf : natmap_wf natmap_car
 }.
-Arguments NatMap {_} _ _.
-Arguments natmap_car {_} _.
-Arguments natmap_prf {_} _.
+Arguments NatMap {_} _ _ : assert.
+Arguments natmap_car {_} _ : assert.
+Arguments natmap_prf {_} _ : assert.
 Lemma natmap_eq {A} (m1 m2 : natmap A) :
   m1 = m2 ↔ natmap_car m1 = natmap_car m2.
 Proof.
diff --git a/theories/nmap.v b/theories/nmap.v
index 3364133d221d096f4986c4e7057331d260bc58af..8ab9fa8767c49043bd6da90559752c3749748036 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -9,9 +9,9 @@ Set Default Proof Using "Type".
 Local Open Scope N_scope.
 
 Record Nmap (A : Type) : Type := NMap { Nmap_0 : option A; Nmap_pos : Pmap A }.
-Arguments Nmap_0 {_} _.
-Arguments Nmap_pos {_} _.
-Arguments NMap {_} _ _.
+Arguments Nmap_0 {_} _ : assert.
+Arguments Nmap_pos {_} _ : assert.
+Arguments NMap {_} _ _ : assert.
 
 Instance Nmap_eq_dec `{EqDecision A} : EqDecision (Nmap A).
 Proof.
diff --git a/theories/numbers.v b/theories/numbers.v
index 885d2dbac54b86d48f398337895537da4b1c480b..c451c91d80884a902c5b6063cf852edb67a8e029 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -14,7 +14,7 @@ Instance comparison_eq_dec : EqDecision comparison.
 Proof. solve_decision. Defined.
 
 (** * Notations and properties of [nat] *)
-Arguments minus !_ !_ /.
+Arguments minus !_ !_ / : assert.
 Reserved Notation "x ≤ y ≤ z" (at level 70, y at next level).
 Reserved Notation "x ≤ y < z" (at level 70, y at next level).
 Reserved Notation "x < y < z" (at level 70, y at next level).
@@ -212,7 +212,7 @@ Notation "(<)" := N.lt (only parsing) : N_scope.
 Infix "`div`" := N.div (at level 35) : N_scope.
 Infix "`mod`" := N.modulo (at level 35) : N_scope.
 
-Arguments N.add _ _ : simpl never.
+Arguments N.add : simpl never.
 
 Instance Npos_inj : Inj (=) (=) Npos.
 Proof. by injection 1. Qed.
@@ -281,15 +281,15 @@ Qed.
 
 (* Note that we cannot disable simpl for [Z.of_nat] as that would break
 tactics as [lia]. *)
-Arguments Z.to_nat _ : simpl never.
-Arguments Z.mul _ _ : simpl never.
-Arguments Z.add _ _ : simpl never.
-Arguments Z.opp _ : simpl never.
-Arguments Z.pow _ _ : simpl never.
-Arguments Z.div _ _ : simpl never.
-Arguments Z.modulo _ _ : simpl never.
-Arguments Z.quot _ _ : simpl never.
-Arguments Z.rem _ _ : simpl never.
+Arguments Z.to_nat : simpl never.
+Arguments Z.mul : simpl never.
+Arguments Z.add : simpl never.
+Arguments Z.opp : simpl never.
+Arguments Z.pow : simpl never.
+Arguments Z.div : simpl never.
+Arguments Z.modulo : simpl never.
+Arguments Z.quot : simpl never.
+Arguments Z.rem : simpl never.
 
 Lemma Z_to_nat_neq_0_pos x : Z.to_nat x ≠ 0%nat → 0 < x.
 Proof. by destruct x. Qed.
@@ -362,7 +362,7 @@ Notation "(≤)" := Qcle (only parsing) : Qc_scope.
 Notation "(<)" := Qclt (only parsing) : Qc_scope.
 
 Hint Extern 1 (_ ≤ _) => reflexivity || discriminate.
-Arguments Qred _ : simpl never.
+Arguments Qred : simpl never.
 
 Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec.
 Program Instance Qc_le_dec (x y : Qc) : Decision (x ≤ y) :=
@@ -512,7 +512,7 @@ Record Qp := mk_Qp { Qp_car :> Qc ; Qp_prf : (0 < Qp_car)%Qc }.
 Hint Resolve Qp_prf.
 Delimit Scope Qp_scope with Qp.
 Bind Scope Qp_scope with Qp.
-Arguments Qp_car _%Qp.
+Arguments Qp_car _%Qp : assert.
 
 Definition Qp_one : Qp := mk_Qp 1 eq_refl.
 Program Definition Qp_plus (x y : Qp) : Qp := mk_Qp (x + y) _.
diff --git a/theories/option.v b/theories/option.v
index 7df582ef8cb03d3bb0ed8b7b3ae4402f0710a923..7a2c27f93058fa41508a092202182c643a68b5a6 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -24,7 +24,7 @@ Proof. congruence. Qed.
 Definition from_option {A B} (f : A → B) (y : B) (mx : option A) : B :=
   match mx with None => y | Some x => f x end.
 Instance: Params (@from_option) 3.
-Arguments from_option {_ _} _ _ !_ /.
+Arguments from_option {_ _} _ _ !_ / : assert.
 
 (* The eliminator again, but with the arguments in different order, which is
 sometimes more convenient. *)
@@ -246,27 +246,27 @@ Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
 not particularly like type level reductions. *)
 Class Maybe {A B : Type} (c : A → B) :=
   maybe : B → option A.
-Arguments maybe {_ _} _ {_} !_ /.
+Arguments maybe {_ _} _ {_} !_ / : assert.
 Class Maybe2 {A1 A2 B : Type} (c : A1 → A2 → B) :=
   maybe2 : B → option (A1 * A2).
-Arguments maybe2 {_ _ _} _ {_} !_ /.
+Arguments maybe2 {_ _ _} _ {_} !_ / : assert.
 Class Maybe3 {A1 A2 A3 B : Type} (c : A1 → A2 → A3 → B) :=
   maybe3 : B → option (A1 * A2 * A3).
-Arguments maybe3 {_ _ _ _} _ {_} !_ /.
+Arguments maybe3 {_ _ _ _} _ {_} !_ / : assert.
 Class Maybe4 {A1 A2 A3 A4 B : Type} (c : A1 → A2 → A3 → A4 → B) :=
   maybe4 : B → option (A1 * A2 * A3 * A4).
-Arguments maybe4 {_ _ _ _ _} _ {_} !_ /.
+Arguments maybe4 {_ _ _ _ _} _ {_} !_ / : assert.
 
 Instance maybe_comp `{Maybe B C c1, Maybe A B c2} : Maybe (c1 ∘ c2) := λ x,
   maybe c1 x ≫= maybe c2.
-Arguments maybe_comp _ _ _ _ _ _ _ !_ /.
+Arguments maybe_comp _ _ _ _ _ _ _ !_ / : assert.
 
 Instance maybe_inl {A B} : Maybe (@inl A B) := λ xy,
   match xy with inl x => Some x | _ => None end.
 Instance maybe_inr {A B} : Maybe (@inr A B) := λ xy,
   match xy with inr y => Some y | _ => None end.
 Instance maybe_Some {A} : Maybe (@Some A) := id.
-Arguments maybe_Some _ !_ /.
+Arguments maybe_Some _ !_ / : assert.
 
 (** * Union, intersection and difference *)
 Instance option_union_with {A} : UnionWith A (option A) := λ f mx my,
diff --git a/theories/pmap.v b/theories/pmap.v
index e9fc2c6e12c86a3fce02aa077a11b28b96610bee..05c9b94c27ce36d01ba7329d592c52699bb1b886 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -24,8 +24,8 @@ all nodes. *)
 Inductive Pmap_raw (A : Type) : Type :=
   | PLeaf: Pmap_raw A
   | PNode: option A → Pmap_raw A → Pmap_raw A → Pmap_raw A.
-Arguments PLeaf {_}.
-Arguments PNode {_} _ _ _.
+Arguments PLeaf {_} : assert.
+Arguments PNode {_} _ _ _ : assert.
 
 Instance Pmap_raw_eq_dec `{EqDecision A} : EqDecision (Pmap_raw A).
 Proof. solve_decision. Defined.
@@ -36,7 +36,7 @@ Fixpoint Pmap_wf {A} (t : Pmap_raw A) : bool :=
   | PNode None PLeaf PLeaf => false
   | PNode _ l r => Pmap_wf l && Pmap_wf r
   end.
-Arguments Pmap_wf _ !_ / : simpl nomatch.
+Arguments Pmap_wf _ !_ / : simpl nomatch, assert.
 Lemma Pmap_wf_l {A} o (l r : Pmap_raw A) : Pmap_wf (PNode o l r) → Pmap_wf l.
 Proof. destruct o, l, r; simpl; rewrite ?andb_True; tauto. Qed.
 Lemma Pmap_wf_r {A} o (l r : Pmap_raw A) : Pmap_wf (PNode o l r) → Pmap_wf r.
@@ -44,7 +44,7 @@ Proof. destruct o, l, r; simpl; rewrite ?andb_True; tauto. Qed.
 Local Hint Immediate Pmap_wf_l Pmap_wf_r.
 Definition PNode' {A} (o : option A) (l r : Pmap_raw A) :=
   match l, o, r with PLeaf, None, PLeaf => PLeaf | _, _, _ => PNode o l r end.
-Arguments PNode' _ _ _ _ : simpl never.
+Arguments PNode' : simpl never.
 Lemma PNode_wf {A} o (l r : Pmap_raw A) :
   Pmap_wf l → Pmap_wf r → Pmap_wf (PNode' o l r).
 Proof. destruct o, l, r; simpl; auto. Qed.
@@ -59,7 +59,7 @@ Instance Plookup_raw {A} : Lookup positive A (Pmap_raw A) :=
   | PLeaf => None
   | PNode o l r => match i with 1 => o | i~0 => l !! i | i~1 => r !! i end
   end.
-Local Arguments lookup _ _ _ _ _ !_ / : simpl nomatch.
+Local Arguments lookup _ _ _ _ _ !_ / : simpl nomatch, assert.
 Fixpoint Psingleton_raw {A} (i : positive) (x : A) : Pmap_raw A :=
   match i with
   | 1 => PNode (Some x) PLeaf PLeaf
@@ -258,9 +258,9 @@ Qed.
 (** Packed version and instance of the finite map type class *)
 Inductive Pmap (A : Type) : Type :=
   PMap { pmap_car : Pmap_raw A; pmap_prf : Pmap_wf pmap_car }.
-Arguments PMap {_} _ _.
-Arguments pmap_car {_} _.
-Arguments pmap_prf {_} _.
+Arguments PMap {_} _ _ : assert.
+Arguments pmap_car {_} _ : assert.
+Arguments pmap_prf {_} _ : assert.
 Lemma Pmap_eq {A} (m1 m2 : Pmap A) : m1 = m2 ↔ pmap_car m1 = pmap_car m2.
 Proof.
   split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
diff --git a/theories/set.v b/theories/set.v
index dbb5a0b28c1a9494acdf43a46b8737f59e101e1b..80f060ec6b7cda4b28cdb1cec45bc5202a6d8c00 100644
--- a/theories/set.v
+++ b/theories/set.v
@@ -6,8 +6,8 @@ Set Default Proof Using "Type".
 
 Record set (A : Type) : Type := mkSet { set_car : A → Prop }.
 Add Printing Constructor set.
-Arguments mkSet {_} _.
-Arguments set_car {_} _ _.
+Arguments mkSet {_} _ : assert.
+Arguments set_car {_} _ _ : assert.
 Notation "{[ x | P ]}" := (mkSet (λ x, P))
   (at level 1, format "{[  x  |  P  ]}") : C_scope.
 
diff --git a/theories/sorting.v b/theories/sorting.v
index 0d8eed644ebfb514d698c7f3567d1def46e80330..ff33637e1e3695f1ca6c3eedad70e2320347c53f 100644
--- a/theories/sorting.v
+++ b/theories/sorting.v
@@ -18,7 +18,7 @@ Section merge_sort.
        if decide_rel R x1 x2 then x1 :: list_merge l1 (x2 :: l2)
        else x2 :: list_merge_aux l2
     end.
-  Global Arguments list_merge !_ !_ /.
+  Global Arguments list_merge !_ !_ / : assert.
 
   Local Notation stack := (list (option (list A))).
   Fixpoint merge_list_to_stack (st : stack) (l : list A) : stack :=
diff --git a/theories/streams.v b/theories/streams.v
index 6d1244e3b716eb117c7a50acd2775a4bb2d47904..747141eb94329c878bef1856ea3d211a0087c5c0 100644
--- a/theories/streams.v
+++ b/theories/streams.v
@@ -4,7 +4,7 @@ From stdpp Require Export tactics.
 Set Default Proof Using "Type".
 
 CoInductive stream (A : Type) : Type := scons : A → stream A → stream A.
-Arguments scons {_} _ _.
+Arguments scons {_} _ _ : assert.
 Delimit Scope stream_scope with stream.
 Bind Scope stream_scope with stream.
 Open Scope stream_scope.
diff --git a/theories/strings.v b/theories/strings.v
index df801e5379af3bc27fbdc378dd44ab76fc4f6002..b028d4942ad855a156675ac79deb5df1f08e3932 100644
--- a/theories/strings.v
+++ b/theories/strings.v
@@ -14,7 +14,7 @@ Notation length := List.length.
 Open Scope string_scope.
 Open Scope list_scope.
 Infix "+:+" := String.append (at level 60, right associativity) : C_scope.
-Arguments String.append _ _ : simpl never.
+Arguments String.append : simpl never.
 
 (** * Decision of equality *)
 Instance assci_eq_dec : EqDecision ascii := ascii_dec.
diff --git a/theories/zmap.v b/theories/zmap.v
index 7c37bb4fd7a8aab4b061269e6b50d33b8f691a32..90c87f5cc094459d3a2e4732700c6ad43d8c8b1a 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -9,10 +9,10 @@ Local Open Scope Z_scope.
 
 Record Zmap (A : Type) : Type :=
   ZMap { Zmap_0 : option A; Zmap_pos : Pmap A; Zmap_neg : Pmap A }.
-Arguments Zmap_0 {_} _.
-Arguments Zmap_pos {_} _.
-Arguments Zmap_neg {_} _.
-Arguments ZMap {_} _ _ _.
+Arguments Zmap_0 {_} _ : assert.
+Arguments Zmap_pos {_} _ : assert.
+Arguments Zmap_neg {_} _ : assert.
+Arguments ZMap {_} _ _ _ : assert.
 
 Instance Zmap_eq_dec `{EqDecision A} : EqDecision (Zmap A).
 Proof.