From 24aef2fea9481e65d1f6658005ddde25ae9a64ee Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 8 Sep 2017 12:05:13 +0200
Subject: [PATCH] Make uses of Arguments more rubust.

See also Coq bug #5712.
---
 theories/base.v          | 112 +++++++++++++++++++--------------------
 theories/bset.v          |   5 +-
 theories/coPset.v        |  10 ++--
 theories/collections.v   |   2 +-
 theories/fin.v           |   2 +-
 theories/finite.v        |  10 ++--
 theories/gmap.v          |   4 +-
 theories/gmultiset.v     |   4 +-
 theories/hashset.v       |   4 +-
 theories/hlist.v         |   2 +-
 theories/list.v          |  28 +++++-----
 theories/listset.v       |   4 +-
 theories/listset_nodup.v |   6 +--
 theories/mapset.v        |   7 +--
 theories/natmap.v        |   6 +--
 theories/nmap.v          |   6 +--
 theories/numbers.v       |  26 ++++-----
 theories/option.v        |  14 ++---
 theories/pmap.v          |  16 +++---
 theories/set.v           |   4 +-
 theories/sorting.v       |   2 +-
 theories/streams.v       |   2 +-
 theories/strings.v       |   2 +-
 theories/zmap.v          |   8 +--
 24 files changed, 144 insertions(+), 142 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index c0d9b428..323dd30d 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 eedd1466..f3f0d828 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 f0bdf929..68b8466f 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 37ce45f2..bb6c4b5f 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 888825cb..4b8cdd0a 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 b68fc619..0a1dff9c 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 4572c905..fe7ddf77 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 01040043..084dfdca 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 b84c1f08..59c5506b 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 e36296e6..90a9830f 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 943ef182..5f3bf784 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 f143e66d..4649ede5 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 edffa54d..dbfb2d62 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 193ab9a9..bb44b671 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 87802090..daa00e46 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 3364133d..8ab9fa87 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 885d2dba..c451c91d 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 7df582ef..7a2c27f9 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 e9fc2c6e..05c9b94c 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 dbb5a0b2..80f060ec 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 0d8eed64..ff33637e 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 6d1244e3..747141eb 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 df801e53..b028d494 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 7c37bb4f..90c87f5c 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.
-- 
GitLab