diff --git a/Core/Configuration.v b/Core/Configuration.v
index 56b19886fb3f0f34182a7cf92a918208ab63d5dd..804cb3461b8e3df3d4574e0d66c8895d499d44d5 100644
--- a/Core/Configuration.v
+++ b/Core/Configuration.v
@@ -146,7 +146,7 @@ Definition on_loc pt (config : configuration) :=
   List.filter (fun id => get_location (config id) ==b pt) names.
 
 Global Instance on_loc_compat : Proper (equiv ==> equiv ==> Logic.eq) on_loc.
-Proof.
+Proof using.
 intros pt1 pt2 Hpt config1 config2 Hconfig. unfold on_loc.
 apply filter_extensionality_compat; trivial; [].
 intros x id ?; subst x. unfold equiv_decb.
@@ -154,13 +154,13 @@ repeat destruct_match; trivial; rewrite Hconfig, Hpt in *; contradiction.
 Qed.
 
 Lemma on_loc_spec : forall pt config id, List.In id (on_loc pt config) <-> get_location (config id) == pt.
-Proof.
+Proof using.
 intros pt config id. unfold on_loc, equiv_decb. rewrite filter_In.
 destruct_match; intuition; apply In_names.
 Qed.
 
 Lemma on_loc_NoDup : forall pt config, NoDup (on_loc pt config).
-Proof. intros pt config. apply NoDup_filter, names_NoDup. Qed.
+Proof using. intros pt config. apply NoDup_filter, names_NoDup. Qed.
 
 (** The list of occupied locations inside a configuration *)
 Definition occupied config :=
@@ -168,7 +168,7 @@ Definition occupied config :=
 
 Lemma occupied_spec : forall pt config,
   InA equiv pt (occupied config) <-> exists id, get_location (config id) == pt.
-Proof.
+Proof using.
 intros pt config. unfold occupied.
 rewrite (proj1 (removeA_dups_spec equiv_dec _)), InA_map_iff; autoclass; [].
 split.
@@ -178,7 +178,7 @@ split.
 Qed.
 
 Global Instance occupied_compat : Proper (equiv ==> eqlistA equiv) occupied.
-Proof.
+Proof using.
 intros config1 config2 Hconfig. unfold occupied.
 induction names as [| id l]; try reflexivity; [].
 cbn.
@@ -195,11 +195,11 @@ destruct_match.
 Qed.
 
 Lemma occupied_NoDupA : forall config, NoDupA equiv (occupied config).
-Proof. intro. apply removeA_dups_spec. Qed.
+Proof using. intro. apply removeA_dups_spec. Qed.
 
 Lemma occupied_config_list : forall config,
   equivlistA equiv (occupied config) (map get_location (config_list config)).
-Proof.
+Proof using.
 intro.
 etransitivity; [apply removeA_dups_spec |].
 unfold config_list, Gpos, Bpos, names.
diff --git a/Core/Formalism.v b/Core/Formalism.v
index 30c0cd6db0479fc91ec35418ac14514a933f138d..10159f49916154701b9b9c439ad679e4dc0e385c 100644
--- a/Core/Formalism.v
+++ b/Core/Formalism.v
@@ -231,13 +231,13 @@ apply In_names.
 Qed.
 
 Lemma active_NoDup : forall da, NoDup (active da).
-Proof. intro. apply NoDup_filter, names_NoDup. Qed.
+Proof using. intro. apply NoDup_filter, names_NoDup. Qed.
 
 Lemma idle_NoDup : forall da, NoDup (idle da).
-Proof. intro. apply NoDup_filter, names_NoDup. Qed.
+Proof using. intro. apply NoDup_filter, names_NoDup. Qed.
 
 Lemma active_idle_is_partition : forall da, PermutationA eq names ((active da) ++ (idle da)).
-Proof.
+Proof using.
 intros da. unfold active, idle. induction names as [| id l].
 + reflexivity.
 + cbn. destruct_match; cbn.
@@ -351,11 +351,11 @@ split; intro Hin.
 Qed.
 
 Lemma moving_NoDup : forall r da config, NoDup (moving r da config).
-Proof. intros. apply NoDup_filter, names_NoDup. Qed.
+Proof using. intros. apply NoDup_filter, names_NoDup. Qed.
 
 Lemma moving_dec : forall r da config id,
   {List.In id (moving r da config)} + {~List.In id (moving r da config)}.
-Proof. intros. apply In_dec, names_eq_dec. Qed.
+Proof using. intros. apply In_dec, names_eq_dec. Qed.
 
 (** A fourth subset of robots: stationary ones. *)
 Definition stationary r da config :=
@@ -393,29 +393,29 @@ split; intro Hin.
 Qed.
 
 Lemma stationary_NoDup : forall r da config, NoDup (stationary r da config).
-Proof. intros. apply NoDup_filter, names_NoDup. Qed.
+Proof using. intros. apply NoDup_filter, names_NoDup. Qed.
 
 Lemma stationary_dec : forall r da config id,
   {List.In id (stationary r da config)} + {~List.In id (stationary r da config)}.
-Proof. intros. apply In_dec, names_eq_dec. Qed.
+Proof using. intros. apply In_dec, names_eq_dec. Qed.
 
 Lemma stationary_iff_not_moving : forall r da config id,
   List.In id (stationary r da config) <-> ~ List.In id (moving r da config).
-Proof.
+Proof using.
 intros r da config id. rewrite stationary_spec, moving_spec.
 destruct (get_location (round r da config id) =?= get_location (config id)); intuition.
 Qed.
 
 Corollary moving_or_stationary : forall r da config id,
   List.In id (moving r da config) \/ List.In id (stationary r da config).
-Proof.
+Proof using.
 intros. rewrite stationary_iff_not_moving, moving_spec.
 destruct (get_location (round r da config id) =?= get_location (config id)); intuition.
 Qed.
 
 Corollary moving_stationary_is_partition : forall r da config,
   PermutationA eq names ((moving r da config) ++ (stationary r da config)).
-Proof.
+Proof using.
 intros r da config. unfold moving, stationary.
 induction names as [| id l]; try reflexivity; []; cbn.
 repeat destruct_match; try discriminate.
@@ -459,7 +459,7 @@ Qed.
 
 Lemma changing_dec : forall r da config id,
   {List.In id (changing r da config)} + {~List.In id (changing r da config)}.
-Proof. intros. apply In_dec, names_eq_dec. Qed.
+Proof using. intros. apply In_dec, names_eq_dec. Qed.
 
 Lemma no_changing_same_config : forall r da config,
   changing r da config = List.nil -> round r da config == config.
@@ -530,7 +530,7 @@ Qed.
 
 Corollary moving_active : forall da, SSYNC_da da ->
   forall r config, List.incl (moving r da config) (active da).
-Proof.
+Proof using.
 intros da Hssync r config.
 transitivity (changing r da config).
 + now apply moving_changing.
@@ -575,7 +575,7 @@ Proof using . unfold round. repeat intro. destruct_match_eq Hcase; auto. Qed.
 
 Lemma SSync_inactive_nochange:
   forall r da c id, SSYNC_da da -> activate da id = false -> round r da c id == c id.
-Proof.
+Proof using.
   intros r da c id h_ssync h. 
   remember (round r da c) as f.
   assert ( f == round r da c) as hequivf.
diff --git a/Util/ListComplements.v b/Util/ListComplements.v
index d394cf62d05fdb4e5a8cc7330e1e1fb4aeec49ed..3bd8d16287945e05154b008300e689b8334013ec 100644
--- a/Util/ListComplements.v
+++ b/Util/ListComplements.v
@@ -155,7 +155,7 @@ intros d [| x l] Hl.
 Qed.
 
 Lemma hd_eqlistA_compat : Proper (eqA ==> eqlistA eqA ==> eqA) (@hd A).
-Proof. intros x y Hxy l1 l2 Hl. now inv Hl; cbn. Qed.
+Proof using . intros x y Hxy l1 l2 Hl. now inv Hl; cbn. Qed.
 
 Lemma last_In : forall l (d : A), l <> List.nil -> List.In (List.last l d) l.
 Proof using .
@@ -380,7 +380,7 @@ Lemma InA_map:
     Proper (eqA ==> eqB) f ->
     forall (l : list A)
            (x : A), InA eqA x l -> InA eqB (f x) (List.map f l).
-Proof.
+Proof using.
   intros f hProper l.
   induction l.
   - intros x hInA.
@@ -400,7 +400,7 @@ Lemma InA_map_not: forall f : A -> B,
     Proper (eqA ==> eqB) f ->
     forall (l : list A)
            (x : A), ~InA eqB (f x) (List.map f l) -> ~InA eqA x l.
-Proof.
+Proof using HeqB.
   intros f hProper l.
   induction l.
   - intros x hnotInB.
@@ -889,7 +889,7 @@ Lemma PermutationA_3_swap : forall l e1 e2 e3 pt1 pt2,
   InA eqA pt1 (e1 :: e2 :: e3 :: l) ->
   InA eqA pt2 (e1 :: e2 :: e3 :: l) ->
   exists pt l', PermutationA eqA (e1 :: e2 :: e3 :: l) (pt1 :: pt2 :: pt :: l').
-Proof.
+Proof using HeqA.
 intros l e1 e2 e3 pt1 pt2 Hdiff Hin1 Hin2.
 pose (l' := e1 :: e2 :: e3 :: l).
 (* assert (Hneq : e1 =/= e2 /\ e1 =/= e3 /\ e2 =/= e3).
@@ -1193,7 +1193,7 @@ intros f g Hfg l1. induction l1 as [| x l1]; intros l2 Hl; simpl.
 Qed.
 
 Lemma filter_false : forall (l : list A), filter (fun _ => false) l = nil.
-Proof. induction l; auto. Qed.
+Proof using. induction l; auto. Qed.
 
 Lemma filter_twice : forall f (l : list A), filter f (filter f l) = filter f l.
 Proof using .
@@ -1510,7 +1510,7 @@ Proof using HeqA. intros. now rewrite <- countA_occ_spec. Qed.
 
 Lemma count_filter_length: forall x l,
     countA_occ x l = length (List.filter (fun a => if eq_dec a x then true else false) l).
-Proof.
+Proof using.
   induction l;auto.
   cbn.
   destruct (eq_dec a x);cbn.
@@ -2046,7 +2046,7 @@ Fixpoint removeA_dups eqA_dec (l : list A) :=
 
 Lemma removeA_dups_spec : forall eqA_dec l,
   equivlistA eqA (removeA_dups eqA_dec l) l /\ NoDupA eqA (removeA_dups eqA_dec l).
-Proof.
+Proof using HeqA.
 intros eqA_dec l.
 induction l; cbn.
 * now split.