diff --git a/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v b/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
index ece8453a0e754772c9069389f74120563bec1dcb..d413a8550f918c0e594754c18e0555c2d7c8398c 100644
--- a/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
+++ b/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
@@ -113,7 +113,8 @@ Arguments dist : simpl never.
 Definition path_R2 := path location.
 Definition paths_in_R2 : location -> path_R2 := local_straight_path.
 (* TODO: understand the warning here. *)
-Coercion paths_in_R2 : location >-> path_R2.
+#[local,warnings="-uniform-inheritance"]
+  Coercion paths_in_R2 : location >-> path_R2.
 
 Instance paths_in_R2_compat : Proper (@equiv _ location_Setoid ==> equiv) paths_in_R2.
 Proof using . intros pt1 pt2 Heq. now rewrite Heq. Qed.
diff --git a/Spaces/EuclideanSpace.v b/Spaces/EuclideanSpace.v
index ceeda43fc195aef13003ed0d2e72bbdee0fd5875..8ceadb0e0b1e52ded20f15d6f91a787dca62a3cb 100644
--- a/Spaces/EuclideanSpace.v
+++ b/Spaces/EuclideanSpace.v
@@ -29,7 +29,7 @@ Class EuclideanSpace (T : Type) {S : Setoid T} {EQ : @EqDec T S} {VS : RealVecto
   inner_product_defined : forall u, inner_product u u = 0%R <-> u == origin}.
 
 Global Existing Instance inner_product_compat.
-Arguments inner_product {T%type} {_} {_} {_} {_} u%VS V%VS.
+Arguments inner_product {T%_type} {_} {_} {_} {_} u%_VS V%_VS.
 Notation "〈 u , v 〉" := (inner_product u v) (format "'〈' u ,  v '〉'"): VectorSpace_scope.
 (* Open Scope VectorSpace_scope. *)
 
@@ -156,7 +156,7 @@ Section PerpendicularResults.
   Qed.
   
 End PerpendicularResults.
-Arguments perpendicular {T%type} {_} {_} {_} {_} u%VS v%VS.
+Arguments perpendicular {T%_type} {_} {_} {_} {_} u%_VS v%_VS.
 Notation "u ⟂ v" := (perpendicular u v) (at level 50, no associativity).
 
 (** *** The norm induced by the [inner_product]  **)
diff --git a/Spaces/RealMetricSpace.v b/Spaces/RealMetricSpace.v
index ad000c65c2a5bbc25860003a78f5135ee79b7524..4ded9998b5b4c1b0ff1ad0b47f8f41b30e43ffd4 100644
--- a/Spaces/RealMetricSpace.v
+++ b/Spaces/RealMetricSpace.v
@@ -22,7 +22,7 @@ Class RealMetricSpace (T : Type) {S : Setoid T} `{@EqDec T S} {VS : RealVectorSp
   dist_sym : forall u v, dist v u = dist u v;
   triang_ineq : forall u v w, (dist u w <= dist u v + dist v w)%R}.
 
-Arguments dist T%type _ _ _ _ u%VS v%VS.
+Arguments dist T%_type _ _ _ _ u%_VS v%_VS.
 
 Global Instance dist_compat `{RealMetricSpace} : Proper (equiv ==> equiv ==> Logic.eq) dist.
 Proof.
diff --git a/Spaces/RealNormedSpace.v b/Spaces/RealNormedSpace.v
index 54529d201ca6831ad06e4b017136686e2097e678..3547ef0f6c3843fb765d5bebda2b73411c8d737e 100644
--- a/Spaces/RealNormedSpace.v
+++ b/Spaces/RealNormedSpace.v
@@ -30,7 +30,7 @@ Class RealNormedSpace (T : Type) {S : Setoid T} {EQ : @EqDec T S} {VS : RealVect
   triang_ineq : forall u v, (norm (add u v) <= norm u + norm v)%R}.
 
 Global Existing Instance norm_compat.
-Arguments norm T%type _ _ _ _ u%VS.
+Arguments norm T%_type _ _ _ _ u%_VS.
 Notation "∥ u ∥" := (norm u) :  VectorSpace_scope.
 
 (** ***  Proofs of derivable properties about RealNormedSpace  **)
@@ -421,4 +421,4 @@ Section BarycenterResults.
   
 End BarycenterResults.
 
-Arguments unitary {T%type} {_} {_} {_} {_} u%VS.
+Arguments unitary {T%_type} {_} {_} {_} {_} u%_VS.
diff --git a/Spaces/RealVectorSpace.v b/Spaces/RealVectorSpace.v
index 15bf3e83e5d2b743ef4fe168dbca6f261d4de224..53c8c624460554a082c3a9bfa6666ff3aaf26c94 100644
--- a/Spaces/RealVectorSpace.v
+++ b/Spaces/RealVectorSpace.v
@@ -51,17 +51,17 @@ Global Existing Instance opp_compat.
 
 Declare Scope VectorSpace_scope.
 Delimit Scope VectorSpace_scope with VS.
-Arguments add T%type _ _ _ u%VS v%VS.
-Arguments mul T%type _ _ _ k%R u%VS.
-Arguments opp T%type _ _ _ u%VS.
-Arguments add_assoc {T} {_} {_} {_} u%VS v%VS w%VS.
-Arguments add_comm {T} {_} {_} {_} u%VS v%VS.
-Arguments add_origin {T} {_} {_} {_} u%VS.
-Arguments add_opp {T} {_} {_} {_} u%VS.
-Arguments mul_distr_add {T} {_} {_} {_} a%R u%VS v%VS.
-Arguments mul_morph {T} {_} {_} {_} a%R b%R u%VS.
-Arguments add_morph {T} {_} {_} {_} a%R b%R u%VS.
-Arguments mul_1 {T} {_} {_} {_} u%VS.
+Arguments add T%_type _ _ _ u%_VS v%_VS.
+Arguments mul T%_type _ _ _ k%_R u%_VS.
+Arguments opp T%_type _ _ _ u%_VS.
+Arguments add_assoc {T} {_} {_} {_} u%_VS v%_VS w%_VS.
+Arguments add_comm {T} {_} {_} {_} u%_VS v%_VS.
+Arguments add_origin {T} {_} {_} {_} u%_VS.
+Arguments add_opp {T} {_} {_} {_} u%_VS.
+Arguments mul_distr_add {T} {_} {_} {_} a%_R u%_VS v%_VS.
+Arguments mul_morph {T} {_} {_} {_} a%_R b%_R u%_VS.
+Arguments add_morph {T} {_} {_} {_} a%_R b%_R u%_VS.
+Arguments mul_1 {T} {_} {_} {_} u%_VS.
 
 Notation "0" := (origin) : VectorSpace_scope.
 Notation "u + v" := (add u v) : VectorSpace_scope.
diff --git a/Util/FMaps/FMapInterface.v b/Util/FMaps/FMapInterface.v
index ee95e963cb6421f8c07ccba3aea4c117d9f4535a..e8495defc32392b02ca0557398c4c563dd287674 100644
--- a/Util/FMaps/FMapInterface.v
+++ b/Util/FMaps/FMapInterface.v
@@ -77,7 +77,7 @@ Class FMap `{EqDec key} := {
   FMap_Setoid : forall `{Setoid elt}, Setoid (dict elt);
   FMap_EqDec :> forall `{EqDec elt}, @EqDec (dict elt) FMap_Setoid *)
 }.
-Arguments dict key%type_scope {S0} {H} {FMap} elt%type_scope.
+Arguments dict key%_type_scope {S0} {H} {FMap} elt%_type_scope.
 
 (** Map notations (see below) are interpreted in scope [map_scope],
    delimited with key [scope]. We bind it to the type [map] and to
@@ -85,18 +85,18 @@ Arguments dict key%type_scope {S0} {H} {FMap} elt%type_scope.
 Declare Scope map_scope.
 Delimit Scope map_scope with map.
 Bind Scope map_scope with dict.
-Arguments MapsTo {key%type_scope} {_} {_} {_} {elt%type_scope} _ _ _%map_scope.
-Arguments is_empty {key%type_scope} {_} {_} {_} {elt%type_scope} _%map_scope.
-Arguments mem {key%type_scope} {_} {_} {_} {elt%type_scope} _ _%map_scope.
-Arguments add {key%type_scope} {_} {_} {_} {elt%type_scope} _ _ _%map_scope.
-Arguments find {key%type_scope} {_} {_} {_} {elt%type_scope} _ _%map_scope.
-Arguments remove {key%type_scope} {_} {_} {_} {elt%type_scope} _ _%map_scope.
-Arguments equal {key%type_scope} {_} {_} {_} {elt%type_scope} _ _%map_scope _%map_scope.
-Arguments map {key%type_scope} {_} {_} {_} {elt%type_scope} {elt'%type_scope} _ _%map_scope.
-Arguments mapi {key%type_scope} {_} {_} {_} {elt%type_scope} {elt'%type_scope} _ _%map_scope.
-Arguments fold {key%type_scope} {_} {_} {_} {elt%type_scope} {_%type_scope} _ _%map_scope _.
-Arguments cardinal {key%type_scope} {_} {_} {_} {elt%type_scope} _%map_scope.
-Arguments elements {key%type_scope} {_} {_} {_} {elt%type_scope} _%map_scope.
+Arguments MapsTo {key%_type_scope} {_} {_} {_} {elt%_type_scope} _ _ _%_map_scope.
+Arguments is_empty {key%_type_scope} {_} {_} {_} {elt%_type_scope} _%_map_scope.
+Arguments mem {key%_type_scope} {_} {_} {_} {elt%_type_scope} _ _%_map_scope.
+Arguments add {key%_type_scope} {_} {_} {_} {elt%_type_scope} _ _ _%_map_scope.
+Arguments find {key%_type_scope} {_} {_} {_} {elt%_type_scope} _ _%_map_scope.
+Arguments remove {key%_type_scope} {_} {_} {_} {elt%_type_scope} _ _%_map_scope.
+Arguments equal {key%_type_scope} {_} {_} {_} {elt%_type_scope} _ _%_map_scope _%_map_scope.
+Arguments map {key%_type_scope} {_} {_} {_} {elt%_type_scope} {elt'%_type_scope} _ _%_map_scope.
+Arguments mapi {key%_type_scope} {_} {_} {_} {elt%_type_scope} {elt'%_type_scope} _ _%_map_scope.
+Arguments fold {key%_type_scope} {_} {_} {_} {elt%_type_scope} {_%_type_scope} _ _%_map_scope _.
+Arguments cardinal {key%_type_scope} {_} {_} {_} {elt%_type_scope} _%_map_scope.
+Arguments elements {key%_type_scope} {_} {_} {_} {elt%_type_scope} _%_map_scope.
 
 (** All projections should be made opaque for tactics using [delta]-conversion,
    otherwise the underlying instances may appear during proofs, which then
diff --git a/Util/FSets/FSetFacts.v b/Util/FSets/FSetFacts.v
index ba04e005541190f71879b6776d50e7da32842fd9..4be6f569920cf611f2c32b027186e5cb9b816524 100644
--- a/Util/FSets/FSetFacts.v
+++ b/Util/FSets/FSetFacts.v
@@ -122,7 +122,7 @@ Section IffSpec.
     Lemma exists_spec : exists_ f s = true <-> Exists (fun x => f x = true) s.
     Proof using HF Hf. split; [eapply exists_2 | eapply exists_1]; eauto. Qed.
   End ForFilter.
-  Arguments InA {A%type_scope} _ _ _.
+  Arguments InA {A%_type_scope} _ _ _.
 
 End IffSpec.
 
diff --git a/Util/FSets/FSetInterface.v b/Util/FSets/FSetInterface.v
index 74e6c2a82516de8dd7c206bced633bd777d9f9c4..0e5c1106efa3524a477d28d12645e92c7b46d223 100644
--- a/Util/FSets/FSetInterface.v
+++ b/Util/FSets/FSetInterface.v
@@ -94,7 +94,7 @@ Class FSet `{EqDec elt} := {
     SpecificOrderedType _ (Equal_pw set elt In) *)
 }.
 
-Arguments set elt%type_scope {_} {_} {FSet}.
+Arguments set elt%_type_scope {_} {_} {FSet}.
 
 (** Set notations (see below) are interpreted in scope [set_scope],
    delimited with elt [scope]. We bind it to the type [set] and to
@@ -102,25 +102,25 @@ Arguments set elt%type_scope {_} {_} {FSet}.
 Declare Scope set_scope.
 Delimit Scope set_scope with set.
 Bind Scope set_scope with set.
-Global Arguments In  {_%type_scope} {_} {_} {_} _ _%set_scope.
-Global Arguments is_empty {_%type_scope} {_} {_} {_} _%set_scope.
-Global Arguments mem {_%type_scope} {_} {_} {_} _ _%set_scope.
-Global Arguments add {_%type_scope} {_} {_} {_} _ _%set_scope.
-Global Arguments remove {_%type_scope} {_} {_} {_} _ _%set_scope.
-Global Arguments union {_%type_scope} {_} {_} {_} _%set_scope _%set_scope.
-Global Arguments inter {_%type_scope} {_} {_} {_} _%set_scope _%set_scope.
-Global Arguments diff {_%type_scope} {_} {_} {_} _%set_scope _%set_scope.
-Global Arguments equal {_%type_scope} {_} {_} {_} _%set_scope _%set_scope.
-Global Arguments subset {_%type_scope} {_} {_} {_} _%set_scope _%set_scope.
-Global Arguments fold {_%type_scope} {_} {_} {_} {_} _ _%set_scope _.
-Global Arguments for_all {_%type_scope} {_} {_} {_} _ _%set_scope.
-Global Arguments exists_ {_%type_scope} {_} {_} {_} _ _%set_scope.
-Global Arguments filter {_%type_scope} {_} {_} {_} _ _%set_scope.
-Global Arguments partition {_%type_scope} {_} {_} {_} _ _%set_scope.
-Global Arguments cardinal {_%type_scope} {_} {_} {_} _%set_scope.
-Global Arguments elements {_%type_scope} {_} {_} {_} _%set_scope.
-Global Arguments choose {_%type_scope} {_} {_} {_} _%set_scope.
-(* Global Arguments min_elt {_%type_scope} {_} {_} {_} _%set_scope. *)
+Global Arguments In  {_%_type_scope} {_} {_} {_} _ _%_set_scope.
+Global Arguments is_empty {_%_type_scope} {_} {_} {_} _%_set_scope.
+Global Arguments mem {_%_type_scope} {_} {_} {_} _ _%_set_scope.
+Global Arguments add {_%_type_scope} {_} {_} {_} _ _%_set_scope.
+Global Arguments remove {_%_type_scope} {_} {_} {_} _ _%_set_scope.
+Global Arguments union {_%_type_scope} {_} {_} {_} _%_set_scope _%_set_scope.
+Global Arguments inter {_%_type_scope} {_} {_} {_} _%_set_scope _%_set_scope.
+Global Arguments diff {_%_type_scope} {_} {_} {_} _%_set_scope _%_set_scope.
+Global Arguments equal {_%_type_scope} {_} {_} {_} _%_set_scope _%_set_scope.
+Global Arguments subset {_%_type_scope} {_} {_} {_} _%_set_scope _%_set_scope.
+Global Arguments fold {_%_type_scope} {_} {_} {_} {_} _ _%_set_scope _.
+Global Arguments for_all {_%_type_scope} {_} {_} {_} _ _%_set_scope.
+Global Arguments exists_ {_%_type_scope} {_} {_} {_} _ _%_set_scope.
+Global Arguments filter {_%_type_scope} {_} {_} {_} _ _%_set_scope.
+Global Arguments partition {_%_type_scope} {_} {_} {_} _ _%_set_scope.
+Global Arguments cardinal {_%_type_scope} {_} {_} {_} _%_set_scope.
+Global Arguments elements {_%_type_scope} {_} {_} {_} _%_set_scope.
+Global Arguments choose {_%_type_scope} {_} {_} {_} _%_set_scope.
+(* Global Arguments min_elt {_%_type_scope} {_} {_} {_} _%_set_scope. *)
 (* Global Arguments max_elt {_%type_scope} {_} {_} {_} _%set_scope. *)
 
 (** All projections should be made opaque for tactics using [delta]-conversion,
@@ -319,7 +319,7 @@ Class FSetSpecs `(F : FSet A) := {
   #[global] FFSetSpecs_elements :: FSetSpecs_elements F;
   #[global] FFSetSpecs_choose :: FSetSpecs_choose F;
   (* #[global] FFSetSpecs_min_elt :: FSetSpecs_min_elt F; *)
-  (* #[global] FFSetSpecs_max_elt :: FSetSpecs_max_elt F *)
+  (* #[global]FFSetSpecs_max_elt :: FSetSpecs_max_elt F *)
 }.
 (* About FSetSpecs. *)
 
diff --git a/Util/ListComplements.v b/Util/ListComplements.v
index e9313e9e13f09191a46e04bdd2aa96d148b006c8..d943bc4a9d2c5033b5923b07f5d0d1df7de182c1 100644
--- a/Util/ListComplements.v
+++ b/Util/ListComplements.v
@@ -32,7 +32,7 @@ Require Import Pactole.Util.NumberComplements.
 
 
 Set Implicit Arguments.
-Arguments PermutationA {A}%type eqA%signature l1%list l2%list.
+Arguments PermutationA {A}%_type eqA%_signature l1%_list l2%_list.
 
 
 (******************************)
diff --git a/Util/SetoidDefs.v b/Util/SetoidDefs.v
index 3a5319bb62fc8cd748b844c1f379cf4fd375543a..ae7881a66e8aa3b4fa7341659ad117e4b677b6c2 100644
--- a/Util/SetoidDefs.v
+++ b/Util/SetoidDefs.v
@@ -44,7 +44,7 @@ Global Instance unit_EqDec : EqDec unit_Setoid := fun x y => match x, y with tt,
 Notation "x == y" := (equiv x y).
 Notation "x == y :> A" := (@equiv A _ x y) (at level 70, y at next level, no associativity, only parsing).
 Arguments complement A R x y /.
-Arguments Proper {A}%type R%signature m.
+Arguments Proper {A}%_type R%_signature m.
 
 Lemma equiv_dec_refl {T U} {S : Setoid T} {E : EqDec S} :
   forall (e : T) (A B : U), (if equiv_dec e e then A else B) = A.
diff --git a/minipactole/minipactole.v b/minipactole/minipactole.v
index 8fd89e3f1f4382967f7c2ed04a692ef7850b2a5c..409c74497aff01a964d1f8edd8ec0f6f24c1977c 100644
--- a/minipactole/minipactole.v
+++ b/minipactole/minipactole.v
@@ -21,8 +21,8 @@ Class State {I:Type} {L:Type} {info:@State_info I} {position:@State_pos L}
       info: I
     }.
 (* Point technique: le dernier argument de pos et info n'est pas implicite. *)
-Arguments pos {I}%type {L}%type {info} {position} State.
-Arguments info {I}%type {L}%type {info} {position} State.
+Arguments pos {I}%_type {L}%_type {info} {position} State.
+Arguments info {I}%_type {L}%_type {info} {position} State.
 
 Module Minipactole. (* comme si c'était dans un autre fichier. *)