diff --git a/CaseStudies/Exploration/ImpossibilityKDividesN.v b/CaseStudies/Exploration/ImpossibilityKDividesN.v
index a428f6e02d753ccf509736731b5690ab05419941..7be6f545c53831d394a563fb1fb1d2e35c1bc2da 100644
--- a/CaseStudies/Exploration/ImpossibilityKDividesN.v
+++ b/CaseStudies/Exploration/ImpossibilityKDividesN.v
@@ -42,10 +42,10 @@ Proof.
   now apply neq_lt. 
 Qed.
 
-Local Hint Resolve h_not_0 k_not_0.
+Local Hint Resolve h_not_0 k_not_0: localDB.
 
 Lemma local_subproof1 : n = k * (n / k).
-Proof using kdn ltc_0_k. apply Nat.div_exact. auto. auto. Qed.
+Proof using kdn ltc_0_k. apply Nat.div_exact. auto with localDB. auto with localDB. Qed.
 
 Lemma local_subproof2 : n / k ≠ 0.
 Proof using kdn ltc_2_n ltc_0_k.
@@ -126,10 +126,10 @@ Proof using kdn ltc_0_k k_inf_n.
       exists (Good id'). split. 2:{ rewrite InA_Leibniz. apply In_names. }
       rewrite <- Hpt. cbn -[create_ref_config BijectionInverse]. split; trivial; [].
       change G with (fin k) in *. unfold create_ref_config, Datatypes.id, id'. apply fin2natI.
-      rewrite 2 subf2nat, 3 mod2fin2nat, Nat.add_mod_idemp_l, 2 (Nat.mod_small (_ * _));auto.
+      rewrite 2 subf2nat, 3 mod2fin2nat, Nat.add_mod_idemp_l, 2 (Nat.mod_small (_ * _));auto with localDB.
       - pattern n at 3 5. rewrite local_subproof1.
         rewrite <- Nat.mul_sub_distr_r, <- Nat.mul_add_distr_r.
-        rewrite Nat.mul_mod_distr_r;try auto.
+        rewrite Nat.mul_mod_distr_r;try auto with localDB.
       - apply local_subproof3, fin_lt.
       - pattern n at 2. rewrite local_subproof1, <- Nat.mul_lt_mono_pos_r; try apply mod2fin_lt; [].
         apply Nat.neq_0_lt_0, local_subproof2.
@@ -141,11 +141,11 @@ Proof using kdn ltc_0_k k_inf_n.
            [];
            apply Nat.div_str_pos; split; trivial; []; now apply Nat.lt_le_incl); try lia ;[].
       rewrite local_subproof1 at 2 4.
-      rewrite <- Nat.mul_sub_distr_r, <- Nat.mul_add_distr_r, Nat.mul_mod_distr_r; auto.
+      rewrite <- Nat.mul_sub_distr_r, <- Nat.mul_add_distr_r, Nat.mul_mod_distr_r; auto with localDB.
       apply Nat.mul_cancel_r; try apply local_subproof2; [].
       rewrite Nat.add_mod_idemp_l, <- Nat.add_assoc, (Nat.add_comm (fin2nat g)), Nat.sub_add;
-      try apply Nat.lt_le_incl, fin_lt;auto.
-      rewrite <- Nat.add_mod_idemp_r, Nat.mod_same, Nat.add_0_r;auto. apply Nat.mod_small, fin_lt.
+      try apply Nat.lt_le_incl, fin_lt;auto with localDB.
+      rewrite <- Nat.add_mod_idemp_r, Nat.mod_same, Nat.add_0_r;auto with localDB. apply Nat.mod_small, fin_lt.
 Qed.
 
 (** The demon activate all robots and shifts their view to be on 0. *)
@@ -253,7 +253,7 @@ Lemma f_config_merge : ∀ config m1 m2,
 Proof using k_inf_n kdn.
   intros. unfold f_config. rewrite map_config_merge; autoclass; [].
   intros id. cbn-[equiv]. rewrite 3 asbmE, <- (addm_mod (config id)), <- mod2fin2nat,
-  <- addmA, addm2nat, mod2fin2nat, Nat.add_mod_idemp_l;auto.
+  <- addmA, addm2nat, mod2fin2nat, Nat.add_mod_idemp_l;auto with localDB.
   apply addm_mod.
 Qed.
 
@@ -303,7 +303,7 @@ Lemma equiv_config_m_sym : ∀ m config1 config2,
   -> equiv_config_m (@oppm 2 n ltc_2_n m) config2 config1.
 Proof using k_inf_n kdn.
   unfold equiv_config_m. intros * Hequiv. unshelve erewrite Hequiv,
-  f_config_merge, <- f_config_modulo, (proj2 (Nat.mod_divide _ _ _));auto.
+  f_config_merge, <- f_config_modulo, (proj2 (Nat.mod_divide _ _ _));auto with localDB.
   symmetry. apply f_config_0. apply divide_addn_oppm.
 Qed.
 
diff --git a/CaseStudies/Gathering/Impossibility.v b/CaseStudies/Gathering/Impossibility.v
index 24d98e249e67ce48e1f324e99383612758b77ab7..355f02431cb723625c7019740c5dc7affdab3d04 100644
--- a/CaseStudies/Gathering/Impossibility.v
+++ b/CaseStudies/Gathering/Impossibility.v
@@ -124,7 +124,7 @@ Definition obs_from_config_spec : forall config (pt : location),
   := WithMultiplicity.obs_from_config_spec.
 
 Definition mk_info : location -> location := id.
-Arguments mk_info _%VectorSpace_scope.
+Arguments mk_info _%_VectorSpace_scope.
 Lemma mk_info_get_location : forall pt, get_location (mk_info pt) == pt.
 Proof using . reflexivity. Qed.
 (* 
diff --git a/CaseStudies/Gathering/InR2/Peleg.v b/CaseStudies/Gathering/InR2/Peleg.v
index 18c9b78d75363c1b3558604df191f28ff19f2cc9..66a3a761d4336c5caffc33f5eb4f823007b0e617 100644
--- a/CaseStudies/Gathering/InR2/Peleg.v
+++ b/CaseStudies/Gathering/InR2/Peleg.v
@@ -110,7 +110,8 @@ Arguments dist : simpl never.
 (* The robot trajectories are straight paths. *)
 Definition path_R2 := path location.
 Definition paths_in_R2 : location -> path_R2 := local_straight_path.
-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.