diff --git a/CaseStudies/Gathering/WithMultiplicityLight.v b/CaseStudies/Gathering/WithMultiplicityLight.v
index bfdca76e9997a920432b530057fe0e03e92ff8d0..09ea4ea62b35f4a321bf102855c280c0ebaf3811 100644
--- a/CaseStudies/Gathering/WithMultiplicityLight.v
+++ b/CaseStudies/Gathering/WithMultiplicityLight.v
@@ -29,7 +29,7 @@ Require Import Pactole.Observations.PairObservation.
 Close Scope R_scope.
 Close Scope VectorSpace_scope.
 Set Implicit Arguments.
-Typeclasses eauto := (bfs) 5.
+Typeclasses eauto := (dfs) 5.
 
 Class Lights := {
   L : Type;
@@ -75,7 +75,7 @@ Definition find_another_location config pt :=
                           (List.map get_location (config_list config))).
 
 Local Instance find_another_location_compat : Proper (equiv ==> equiv ==> equiv) find_another_location.
-Proof.
+Proof using Type.
 intros config1 config2 Hconfig pt1 pt2 Hpt. unfold find_another_location.
 apply hd_eqlistA_compat; trivial; [].
 f_equiv.
@@ -89,7 +89,7 @@ Lemma find_another_location_spec : forall config pt,
   ~gathered_at pt config ->
 (*   (exists id1 id2, get_location (config id1) =/= get_location (config id2)) -> *)
   find_another_location config pt =/= pt.
-Proof.
+Proof using Type.
 intros config pt Hgathered. unfold find_another_location. rewrite config_list_spec, map_map.
 intro Habs. apply Hgathered. intro g. assert (Hg := In_names (Good g)).
 induction names as [| id names]; cbn -[equiv_dec] in *.
@@ -105,7 +105,7 @@ Lemma find_another_location_map : forall f,
   forall Pf config pt,
   find_another_location (map_config (lift (existT _ f Pf)) config) (f pt)
   == f (find_another_location config pt).
-Proof.
+Proof using Type.
 intros f Hf Hf_inj Pf config pt. unfold find_another_location.
 rewrite config_list_map, map_map.
 * induction (config_list config) as [| [x li] l]; cbn.
@@ -130,7 +130,7 @@ Definition obsLight_equiv (o1 o2: obsLight) :=
   colors o1 == colors o2 /\ observer_lght o1 == observer_lght o2.
 
 Instance obsLight_is_equiv: Equivalence obsLight_equiv.
-Proof.
+Proof using Type.
   unfold obsLight_equiv.
   repeat split;auto; try now intuition; try etransitivity; eauto.
 Qed.
@@ -158,7 +158,7 @@ Proof.
 Defined.
 
 #[export] Instance colors_compat2: Proper (equiv ==> equiv) colors.
-Proof.
+Proof using Type.
   intros ? ? ?.
   destruct H.
   assumption.
@@ -166,7 +166,7 @@ Qed.
 
 #[export] Instance colors_compat3: Proper (equiv ==> equiv ==> eq)
                                      (fun x => (multiplicity (colors x))).
-Proof.
+Proof using Type.
   repeat intro.
   destruct H.
   rewrite H.
@@ -191,7 +191,7 @@ Definition obs_from_config2 config (state : location * L) :=
     observer_lght := get_light state |}.
 
 Local Instance obs_from_config2_compat : Proper (equiv ==> equiv ==> equiv) obs_from_config2.
-Proof.
+Proof using Type.
   intros config1 config2 Hconfig state1 state2 Hstate.
   unfold obs_from_config2.
 (* assert (Hstate' := @get_location_compat _ _ _ _ _ Hstate). *)
@@ -216,7 +216,7 @@ Lemma obs_from_config2_map : forall f:location -> location,
     obsf == obs_from_config2 (map_config (fun x => (f (fst x), snd x)) config) (f (fst st), snd st) ->
     observer_lght obsf == observer_lght obs /\
       colors obsf == map (fun x => (f (fst x), snd x)) (colors obs).
-Proof.
+Proof using Type.
   intros f Hf Hf_inj config st obs obsf.
   change (fun x => (f (fst x), snd x)) with (lift (existT _ f I)).
   change (f (fst st), snd st) with (lift (existT _ f I) st).
@@ -267,14 +267,14 @@ Global Instance obs_from_config_compat : Proper (equiv ==> equiv ==> equiv)
 Lemma obs_from_config_fst_ok: forall (st st':(location * L)) (c:configuration),
     (obs_from_config (Observation:=multiset_observation) c st)
     = (fst (obs_from_config (Observation:=@Obs) c st')).
-Proof.
+Proof using Type.
   intros st c. 
   reflexivity.
 Qed.
 
 Lemma cardinal_fst_obs_from_config : forall config state,
   cardinal (fst (obs_from_config (Observation:=Obs) config state)) = nG + nB.
-Proof. intros. cbn -[make_multiset cardinal nB nG location]. apply cardinal_obs_from_config. Qed.
+Proof using Type. intros. cbn -[make_multiset cardinal nB nG location]. apply cardinal_obs_from_config. Qed.
 
 Lemma obs_from_config_ignore_snd_except_observerlight :
   forall (ref_st : location * L) config st,
@@ -283,7 +283,7 @@ Lemma obs_from_config_ignore_snd_except_observerlight :
   obs_from_config (Observation := Obs) config st == (fst o, snd o').
   (* The snd part depends on the color of st/ref_st *)
   (* (fst o, Build_obsLight (fst_lght (snd o)) (snd_lght (snd o)) (snd st)). *)
-Proof. reflexivity. Qed.
+Proof using Type. reflexivity. Qed.
 
 Lemma obs_from_config_fst :forall (ref_st : location * L) config obs1 obs2,
       obs_from_config config ref_st == (obs1, obs2) -> 
@@ -301,7 +301,7 @@ Qed.
 
 Lemma observer_light_get_light: forall config id,
     observer_lght (snd (obs_from_config config (config id))) = get_light (config id).
-Proof. reflexivity. Qed.
+Proof using Type. reflexivity. Qed.
 
 
 Lemma obs_from_ok: forall config st,
@@ -318,7 +318,7 @@ Qed.
 
 Lemma obs_from_ok2: forall config st,
     (!!!(config,st)) == (obs_from_config config (origin,witness), snd (!!!(config,st))).
-Proof.
+Proof using Type.
   intros config st. 
   specialize (@obs_from_config_ignore_snd_except_observerlight st config st) as h.
   cbv zeta in h.
@@ -331,7 +331,7 @@ Definition map_light f (obs : observation (Observation := Obs2)) : observation (
      colors := map (fun x => (f (fst x), snd x)) (colors obs) |}.
 
 Instance map_light_compat : forall f, Proper (equiv ==> equiv) f -> Proper (equiv ==> equiv) (map_light f).
-Proof.
+Proof using Type.
 intros f Hf obs1 obs2 Hobs. unfold map_light.
 split; cbn -[equiv]; try apply Hobs; [].
 apply map_compat.
@@ -341,7 +341,7 @@ Qed.
 
 Lemma map_light_extensionality_compat : forall f g, Proper (equiv ==> equiv) f ->
   (forall x, g x == f x) -> forall m , map_light g m == map_light f m.
-Proof.
+Proof using Type.
 intros f g Hf Hfg m. unfold map_light.
 split; cbn -[equiv]; try reflexivity; [].
 apply map_extensionality_compat.
@@ -351,7 +351,7 @@ Qed.
 
 Lemma map_light_merge : forall f g, Proper (equiv ==> equiv) f -> Proper (equiv ==> equiv) g ->
   forall obs, map_light f (map_light g obs) == map_light (fun x => f (g x)) obs.
-Proof.
+Proof using Type.
 intros f g Hf Hg obs. split; try reflexivity; [].
 unfold map_light. cbn -[equiv]. apply map_merge.
 + intros ? ? Heq. split; try apply Hf; apply Heq.
@@ -359,7 +359,7 @@ unfold map_light. cbn -[equiv]. apply map_merge.
 Qed.
 
 Lemma map_light_id : forall obs, map_light id obs == obs.
-Proof.
+Proof using Type.
 intro obs. unfold map_light. split; try reflexivity; []. cbn -[equiv].
 transitivity (map Datatypes.id (colors obs)); try apply map_id; [].
 apply map_extensionality_compat.
@@ -370,7 +370,7 @@ Qed.
 Lemma map_light_colors : forall f,
   Proper (equiv ==> equiv) f -> Preliminary.injective equiv equiv f ->
   forall obs pt c, (colors (map_light f obs))[(f pt, c)] = (colors obs)[(pt, c)].
-Proof.
+Proof using Type.
 intros f Hf Hinj [] pt c. cbn. change (f pt, c) with ((fun x => (f (fst x), snd x)) (pt, c)).
 apply map_injective_spec.
 + intros x y Hxy. now rewrite Hxy.
@@ -382,19 +382,19 @@ Definition map_obs f (obs : observation) : observation :=
 
 Lemma map_obs_compat : forall f : Bijection.bijection location,
   Proper (equiv ==> equiv) (map_obs f).
-Proof. intros f x y Hxy. unfold map_obs. now rewrite Hxy. Qed.
+Proof using Type. intros f x y Hxy. unfold map_obs. now rewrite Hxy. Qed.
 
 Lemma map_obs_merge : forall (f g : Bijection.bijection location),
   Proper (equiv ==> equiv) f -> Proper (equiv ==> equiv) g ->
   forall obs, map_obs f (map_obs g obs) == map_obs (f ∘ g) obs.
-Proof.
+Proof using Type.
 intros f g Hf Hg obs. unfold map_obs. split; cbn -[equiv].
 + now apply map_merge.
 + now apply map_light_merge.
 Qed.
 
 Lemma map_obs_id : forall obs, map_obs id obs == obs.
-Proof.
+Proof using Type.
 intro obs. unfold map_obs. split; cbn -[equiv].
 + apply map_id.
 + apply map_light_id.
@@ -407,7 +407,7 @@ Lemma obs_from_config_map : forall f : Bijection.bijection location,
     (obs_from_config (map_config (lift (existT precondition f Pf)) config)
            (lift (existT precondition f Pf) st))
     == map_obs f (obs_from_config config st).
-Proof.
+Proof using Type.
 intros f Hf Hf_inj Pf config st. split.
 * assert (Hmap := obs_from_config_map Hf I config).
   do 2 (unfold obs_from_config in *; cbn -[equiv] in *).
@@ -530,8 +530,10 @@ Definition bivalent_on config pt1 pt2 :=
   /\ length (occupied config) = 2
   /\ length (on_loc pt1 config) = length (on_loc pt2 config).
 
+Typeclasses eauto := (dfs) 5.
+
 Global Instance bivalent_on_compat : Proper (equiv ==> equiv ==> equiv ==> iff) bivalent_on.
-Proof.
+Proof using Type.
 intros config1 config2 Hconfig pt1 pt1' Hpt1 pt2 pt2' Hpt2.
 unfold bivalent_on.
 setoid_rewrite Hconfig. setoid_rewrite Hpt1. setoid_rewrite Hpt2.
@@ -540,7 +542,7 @@ Qed.
 
 Lemma bivalent_on_bivalent : forall config pt1 pt2,
   bivalent_on config pt1 pt2 -> bivalent config.
-Proof.
+Proof using Type.
 intros config pt1 pt2 [Hloc [Hoccupied Hsame]].
 rewrite <- 2 (obs_from_config_on_loc _ (origin, witness)) in Hsame.
 assert (Hother : forall pt, pt =/= pt1 -> pt =/= pt2 -> (!! config)[pt] = 0).
@@ -587,7 +589,7 @@ Definition color_bivalent_on config pt1 pt2 :=
       l_list.
 
 Global Instance color_bivalent_on_compat : Proper (equiv ==> equiv ==> equiv ==> iff) color_bivalent_on.
-Proof.
+Proof using Type.
 intros ? ? Heq1 ? ? Heq2 ? ? Heq3.
 unfold color_bivalent_on. rewrite 2 Forall_forall.
 setoid_rewrite Heq1. setoid_rewrite Heq2. setoid_rewrite Heq3.
@@ -599,7 +601,7 @@ Qed.
 (* We need to unfold [obs_is_ok] for rewriting *)
 Lemma obs_from_config_fst_spec : forall (config : configuration) st (pt : location),
   (fst (!!! (config,st)))[pt] = countA_occ _ equiv_dec pt (List.map fst (config_list config)).
-Proof. intros. now destruct (obs_from_config_spec config (pt, witness)) as [Hok _]. Qed.
+Proof using Type. intros. now destruct (obs_from_config_spec config (pt, witness)) as [Hok _]. Qed.
 
 Lemma obs_non_nil : 2 <= nG+nB -> forall config st,
   fst (!!! (config,st)) =/= MMultisetInterface.empty.
@@ -614,7 +616,7 @@ Qed.
 
 Local Instance obs_compat : forall pt,
   Proper (equiv ==> eq) (fun obs : location * L => if fst obs =?= pt then true else false).
-Proof.
+Proof using Type.
 intros pt [] [] []. cbn in *.
 repeat destruct_match; auto; exfalso; apply H1 || apply H2; etransitivity; try eassumption; eauto.
 Qed.
@@ -628,7 +630,7 @@ Definition bivalent_obs (obs : observation) : bool :=
   end.
 
 Instance bivalent_obs_compat: Proper (equiv ==> eq) bivalent_obs.
-Proof.
+Proof using Type.
 intros [o1 o1'] [o2 o2'] [Hfst Hsnd]. unfold bivalent_obs. cbn [fst snd] in *.
 assert (Hperm := support_compat Hfst).
 assert (Hlen := PermutationA_length Hperm).
@@ -755,7 +757,7 @@ Qed.
 Lemma bivalent_obs_size : forall obs,
   bivalent_obs obs = true ->
   length (support (elt := location) (fst obs)) = 2.
-Proof.
+Proof using Type.
 intros [obs_loc ?]. unfold bivalent_obs. cbn [fst].
 repeat destruct_match; discriminate || reflexivity.
 Qed.
@@ -763,7 +765,7 @@ Qed.
 Corollary bivalent_size : forall config st,
   bivalent config ->
   length (support (elt := location) (fst (obs_from_config config st))) = 2.
-Proof. intros config st. rewrite <- bivalent_obs_spec. apply bivalent_obs_size. Qed.
+Proof using Type. intros config st. rewrite <- bivalent_obs_spec. apply bivalent_obs_size. Qed.
 
 Lemma bivalent_support : forall config, bivalent config ->
   forall st (pt1 pt2 : location),
@@ -771,7 +773,7 @@ Lemma bivalent_support : forall config, bivalent config ->
     In pt1 (fst (Obs.(obs_from_config) config st)) ->
     In pt2 (fst (obs_from_config config st)) ->
     PermutationA equiv (support (fst (Obs.(obs_from_config) config st))) (cons pt1 (cons pt2 nil)).
-Proof.
+Proof using Type.
 intros config Hbivalent st pt1 pt2 Hdiff Hpt1 Hpt2.
 symmetry.
 apply NoDupA_inclA_length_PermutationA; autoclass.
@@ -807,7 +809,7 @@ Lemma PermutationA_2_gen :
       PermutationA eqA l (x' :: y' :: nil) ->
       exists x y, (eqA x x' /\ eqA y y' \/ eqA x y' /\ eqA y x')
                   /\ l = (x :: y :: nil).
-Proof.
+Proof using Type.
   intros A eqA HequiveqA l x' y' h_permut. 
   specialize (@PermutationA_length _ _ _ _ h_permut) as h_length.
   destruct l as [ | e1 [ | e2 [ | e3 l3]]]; cbn in h_length; try discriminate.
@@ -820,7 +822,7 @@ Qed.
 (* TODO: improve proofs *)
 Local Lemma bivalent_obs_map: forall o whatever (f : Bijection.bijection _),
     bivalent_obs o = true -> bivalent_obs ((map f (fst o)),whatever) = true.
-Proof.
+Proof using Type.
   intros o whatever f H0.
   assert (Hbivalent := H0).
 
@@ -854,7 +856,7 @@ Qed.
 
 Local Lemma bivalent_obs_map_inv: forall o whatever (f : Bijection.bijection _),
     bivalent_obs ((map f (fst o)),whatever) = true -> bivalent_obs o = true.
-Proof.
+Proof using Type.
   intros o whatever f h_bivopsmap.
   assert (Proper (equiv ==> equiv) (λ x0 : location, Bijection.retraction f (f x0))).
   { repeat intro.
@@ -905,7 +907,7 @@ Qed.
 
 Corollary bivalent_obs_morph_strong : forall obs (f : Bijection.bijection _) whatever,
   bivalent_obs ((map f (fst obs)), whatever) = bivalent_obs obs.
-Proof.
+Proof using Type.
 intros obs f whatever.
 destruct (bivalent_obs obs) eqn:Hcase.
 + now apply bivalent_obs_map.
@@ -915,13 +917,13 @@ Qed.
 
 Corollary bivalent_obs_morph : forall f obs,
   bivalent_obs (map_obs f obs) = bivalent_obs obs.
-Proof. intros. apply bivalent_obs_morph_strong. Qed.
+Proof using Type. intros. apply bivalent_obs_morph_strong. Qed.
 
 Lemma permut_forallb_ext:
   (forall A (l: list A) (f g: A -> bool),
       (forall a: A, f a = g a) -> 
       forallb f l = forallb g l).
-Proof.
+Proof using Type.
   intros A l f g H.
   induction l;auto.
   cbn.
@@ -933,7 +935,7 @@ Lemma permut_forallb:
       (forall a: A, f a = g a) -> 
       PermutationA eq l1 l2 -> 
       forallb f l1 = forallb g l2).
-Proof.
+Proof using Type.
   intros A l3 l4 f g Hext Hpermut. 
   induction Hpermut.
   + reflexivity.
@@ -952,7 +954,7 @@ Proof.
 Qed.
 
 Instance color_bivalent_obs_compat: Proper (equiv ==> eq) color_bivalent_obs.
-Proof.
+Proof using Type.
   intros [o1 o1'] [o2 o2'] [Hfst Hsnd].
   unfold color_bivalent_obs.
   cbn [fst snd] in *.
@@ -990,7 +992,7 @@ Qed.
 
 Lemma color_bivalent_obs_bivalent_obs:
   forall o, color_bivalent_obs o = true -> bivalent_obs o = true.
-Proof.
+Proof using Type.
   intros o h.
   unfold color_bivalent_obs, bivalent_obs in *.
   destruct (support (fst o)) as [ | e1 [ | e2 [ | e3 l3]] ];try now (contradict h;auto).
@@ -1131,7 +1133,7 @@ Qed.
 *)
 Lemma color_bivalent_bivalent : forall config,
   color_bivalent config -> bivalent config.
-Proof.
+Proof using Type.
   intros config H. 
   unfold bivalent.
   unfold color_bivalent in H.
@@ -1144,7 +1146,7 @@ Qed.
 
 Corollary color_bivalent_even : forall config,
   color_bivalent config -> Nat.Even (nG + nB).
-Proof.
+Proof using Type.
 intros config Hconfig. apply color_bivalent_bivalent in Hconfig.
 now destruct Hconfig.
 Qed.
@@ -1228,17 +1230,17 @@ Arguments bivalent_same_location config st {pt1} {pt2} pt3 _ _ _ _ _.
 Lemma bivalent_other_locs : forall config, bivalent config ->
   forall pt1 pt2, pt1 =/= pt2 -> In pt1 (!! config) -> In pt2 (!! config) ->
   forall pt, pt =/= pt1 -> pt =/= pt2 -> (!! config)[pt] = 0.
-Proof.
+Proof using Type.
 intros config Hbivalent pt1 pt2 Hdiff Hpt1 Hpt2 pt Hneq1 Hneq2.
 destruct (Nat.eq_0_gt_0_cases (!!config)[pt]) as [| Hlt]; trivial; [].
 elim Hdiff. apply (bivalent_same_location _ _ pt Hbivalent Hpt1 Hpt2); intuition.
 Qed.
 
 Lemma obs_fst : forall config, !! config == fst (!!!(config, (origin, witness))).
-Proof. reflexivity. Qed.
+Proof using Type. reflexivity. Qed.
 
 Lemma fold_obs_fst : forall st config, fst (!!!(config, st)) == !! config.
-Proof. reflexivity. Qed.
+Proof using Type. reflexivity. Qed.
 
 Definition bivalent_extended (config : configuration) :=
   let n := nG + nB in
@@ -1250,7 +1252,7 @@ Definition bivalent_extended (config : configuration) :=
 
 Lemma extend_bivalent : forall config,
   bivalent config <-> bivalent_extended config.
-Proof.
+Proof using Type.
 intro config. split; intro Hbivalent.
 * assert (Hlen := bivalent_size (origin, witness) Hbivalent).
   rewrite <- obs_fst in Hlen.
@@ -1287,7 +1289,7 @@ Qed.
 Lemma bivalent_min: forall c,
     bivalent c ->
     nG + nB >= 2.
-Proof.
+Proof using Type.
   intros c h_biv. 
   unfold bivalent in h_biv.
   now decompose [and] h_biv.
@@ -1297,7 +1299,7 @@ Qed.
 Lemma biv_col_size: forall c,
     color_bivalent c -> 
     size (!! c) = 2.
-Proof.
+Proof using Type.
   intros c h_bivcol. 
   apply color_bivalent_bivalent in h_bivcol.
   apply bivalent_size with (st := (origin,witness)) in h_bivcol.
@@ -1309,7 +1311,7 @@ Qed.
 Lemma biv_col_supp: forall c,
     color_bivalent c -> 
     exists pt1 pt2, support (!! c) = (pt1::pt2::nil).
-Proof.
+Proof using Type.
   intros c h_bivcol. 
   specialize (biv_col_size h_bivcol) as h_size.
   rewrite size_spec in h_size.
@@ -1320,7 +1322,7 @@ Qed.
 Lemma biv_col_supp2: forall c st,
     color_bivalent c -> 
     exists pt1 pt2, support (fst (!!! (c,st))) = (pt1::pt2::nil).
-Proof.
+Proof using Type.
   intros c st h_bivcol.
   specialize (biv_col_size h_bivcol) as h_size.
   rewrite size_spec in h_size.
@@ -1332,7 +1334,7 @@ Lemma colors_indep:
   forall c st st',
     (colors (snd (!!! (c, st))))
     == (colors (snd (!!! (c, st')))).
-Proof.
+Proof using Type.
   intros c st st'. 
   destruct (!!! (c, st)) eqn:heq.
   destruct (!!! (c, st')) eqn:heq'.
@@ -1346,7 +1348,7 @@ Qed.
 
 #[export]
 Instance pair_compat_ours {A B} {SA : Setoid A} {SB : Setoid B}: Proper (equiv ==> equiv ==> equiv) (@pair A B).
-Proof.
+Proof using Type.
   repeat intro.
   split;cbn;auto.
 Qed.
@@ -1540,7 +1542,7 @@ Qed.
 
 Lemma bivalent_sim : forall (sim : similarity location) Psim obs,
   bivalent (map_config (lift (existT precondition sim Psim)) obs) <-> bivalent obs.
-Proof.
+Proof using Type.
 intros sim Psim obs.
 rewrite <- 2 bivalent_obs_spec; trivial; [].
 rewrite obs_from_config_map with (st := (origin, witness)).
@@ -1551,7 +1553,7 @@ Qed.
 
 Lemma color_bivalent_obs_morph : forall f obs,
   color_bivalent_obs (map_obs f obs) = color_bivalent_obs obs.
-Proof.
+Proof using Type.
 intros f [obs_loc obs_light].
 unfold color_bivalent_obs in *. cbn -[equiv support].
 assert (Hperm := map_injective_support (Bijection.section_compat f) (Bijection.injective f) obs_loc).
@@ -1585,7 +1587,7 @@ Qed.
 
 
 Property state_in_config : forall config pt id, In (config id) (colors (snd (Obs.(obs_from_config) config pt))).
-Proof.
+Proof using Type.
 intros config pt id. unfold obs_from_config. simpl. unfold In.
 rewrite make_multiset_spec. rewrite (countA_occ_pos _).
 change (@prod_Setoid (@location Loc) (@L Lght) (@location_Setoid Loc) (@L_Setoid Lght))
@@ -1595,7 +1597,7 @@ Qed.
 
 Property obs_from_config_In_gen : forall (config:configuration) (pt:location * L) (l:location * L),
   In l (colors (snd (Obs.(obs_from_config) config pt))) <-> exists id, (config id) == l.
-Proof.
+Proof using InaFun UpdFun.
 intros config pt l. split; intro Hin.
 + assert (Heq := obs_from_config_spec config pt).
   unfold obs_is_ok, obs_from_config, multiset_observation in *.
diff --git a/minipactole/minipactole.v b/minipactole/minipactole.v
index aef316fbf954d6fa0d6932982b2b807184e030fd..15fca270a42984f0cb57c5530e0cbf2e0afe95b9 100644
--- a/minipactole/minipactole.v
+++ b/minipactole/minipactole.v
@@ -9,7 +9,7 @@ Open Scope R_scope.
 Inductive ident:Type := A | B. (* Nous avons seulement 2 robots. *)
 
 Definition position := (R*R)%type. (*les coordonnées dans le plan euclidien.*)
-
+Unset Automatic Proposition Inductives.
 Class State_info {info:Type}:Type := mkStI { }. (* Paramètre du modèle *)
 Class State_pos {pos:Type}:Type := mkStP { }. (* Paramètre du modèle *)