diff --git a/Core/Formalism.v b/Core/Formalism.v
index cf10b45596bf3b7acc8d01ee9fce7b10ef2db211..656d76d6d7df6cfac10fb10b4dfd360bd83415cf 100644
--- a/Core/Formalism.v
+++ b/Core/Formalism.v
@@ -51,11 +51,11 @@ Definition execution := Stream.t configuration.
 
 (** Good robots have a common program, which we call a [robogram].
     It returns some piece of information (e.g. target location) which must form a setoid. *)
-Class robot_choice := { robot_choice_Setoid :> Setoid Trobot }.
+Class robot_choice := { #[global] robot_choice_Setoid :: Setoid Trobot }.
 
 Record robogram `{robot_choice} := {
   pgm :> observation -> Trobot;
-  pgm_compat :> Proper (equiv ==> equiv) pgm}.
+  #[global] pgm_compat :: Proper (equiv ==> equiv) pgm}.
 
 Global Instance robogram_Setoid `{robot_choice} : Setoid robogram.
 simple refine {| equiv := fun r1 r2 => forall s, pgm r1 s == pgm r2 s |};
@@ -87,28 +87,28 @@ Qed.
     It must at least contain a bijection to compute the change of frame of reference.  *)
 Class frame_choice := {
   frame_choice_bijection : Tframe -> bijection location;
-  frame_choice_Setoid :> Setoid Tframe;
-  frame_choice_bijection_compat :> Proper (equiv ==> equiv) frame_choice_bijection }.
+  #[global] frame_choice_Setoid :: Setoid Tframe;
+  #[global] frame_choice_bijection_compat :: Proper (equiv ==> equiv) frame_choice_bijection }.
 
 (** An [update_choice] represents the choices the demon makes after a robot computation. *)
 Class update_choice := {
-  update_choice_Setoid :> Setoid Tactive;
-  update_choice_EqDec :> EqDec update_choice_Setoid }.
+  #[global] update_choice_Setoid :: Setoid Tactive;
+  #[global] update_choice_EqDec :: EqDec update_choice_Setoid }.
 
 (** An [inactive_choice] represents the choices the demon makes when a robot is not activated. *)
 Class inactive_choice := {
-  inactive_choice_Setoid :> Setoid Tinactive;
-  inactive_choice_EqDec :> EqDec inactive_choice_Setoid }.
+  #[global] inactive_choice_Setoid :: Setoid Tinactive;
+  #[global] inactive_choice_EqDec :: EqDec inactive_choice_Setoid }.
 
 (** These choices are then used by update functions that depend on the model. *)
 (* RMK: we cannot combine them toghether otherwise we get dependencies on the other parameter. *)
 Class update_function `{robot_choice} `{frame_choice} `{update_choice} := {
   update : configuration -> G -> Tframe -> Trobot -> Tactive -> info;
-  update_compat :> Proper (equiv ==> Logic.eq ==> equiv ==> equiv ==> equiv ==> equiv) update }.
+  #[global] update_compat :: Proper (equiv ==> Logic.eq ==> equiv ==> equiv ==> equiv ==> equiv) update }.
 
 Class inactive_function  `{inactive_choice} := {
   inactive : configuration -> ident -> Tinactive -> info;
-  inactive_compat :> Proper (equiv ==> Logic.eq ==> equiv ==> equiv) inactive }.
+  #[global] inactive_compat :: Proper (equiv ==> Logic.eq ==> equiv ==> equiv) inactive }.
 
 Context {RC : robot_choice}.
 Context {FC : frame_choice}.
diff --git a/Core/State.v b/Core/State.v
index d72d5214dd9c107533f56f41d75655bdb140971d..b8cec83788aeec79b85c22804772baaa5f6390db 100644
--- a/Core/State.v
+++ b/Core/State.v
@@ -34,8 +34,8 @@ Require Import Pactole.Core.Identifiers.
     Instead, the user must explicitely provide the instance. *)
 Class Location := {
   location : Type;
-  location_Setoid :> Setoid location;
-  location_EqDec :> EqDec location_Setoid }.
+  #[global] location_Setoid :: Setoid location;
+  #[global] location_EqDec :: EqDec location_Setoid }.
 
 Definition make_Location (T : Type) `{EqDec T} := {| location := T |}.
 Arguments make_Location T {_} {_}.
@@ -54,15 +54,15 @@ Arguments make_Location T {_} {_}.
 Class State `{Location} info := {
   get_location : info -> location;
   (** States are equipped with a decidable equality *)
-  state_Setoid :> Setoid info;
-  state_EqDec :> EqDec state_Setoid;
+  #[global] state_Setoid :: Setoid info;
+  #[global] state_EqDec :: EqDec state_Setoid;
   (** Lifting a change of frame from a location to a full state, under some precondition *)
   precondition : (location -> location) -> Type;
   lift : sigT precondition -> info -> info;
   get_location_lift : forall f state, get_location (lift f state) == projT1 f (get_location state);
   (** Compatibility properties *)
-  get_location_compat :> Proper (equiv ==> equiv) get_location;
-  lift_compat :>
+  #[global] get_location_compat :: Proper (equiv ==> equiv) get_location;
+  #[global] lift_compat ::
     Proper ((equiv ==> equiv)%signature @@ (@projT1 _ precondition) ==> equiv ==> equiv) lift }.
 (* We cannot have [lift_compat :> Proper (equiv ==> equiv ==> equiv) lift]
    because we also need extensionality in the input function, which function's [equiv] has not. *)
diff --git a/Models/Flexible.v b/Models/Flexible.v
index afb6771197ada3f16cb821a4aefd04ba69d55e76..b5f48b35f9a6f4789ea7db9ea728cef29c3b0430 100644
--- a/Models/Flexible.v
+++ b/Models/Flexible.v
@@ -48,7 +48,7 @@ Instance Frame : frame_choice (similarity location) := FrameChoiceSimilarity.
 
 Class FlexibleChoice `{update_choice Tactive} := {
   move_ratio : Tactive -> ratio;
-  move_ratio_compat :> Proper (@equiv Tactive update_choice_Setoid ==> @equiv _ (sig_Setoid _)) move_ratio }.
+  #[global] move_ratio_compat :: Proper (@equiv Tactive update_choice_Setoid ==> @equiv _ (sig_Setoid _)) move_ratio }.
 
 (** Flexible moves are parametrized by a minimum distance [delta] that robots must move when they are activated. *)
 Class FlexibleSetting `{FlexibleChoice}
diff --git a/Models/GraphEquivalence.v b/Models/GraphEquivalence.v
index 8ea39ff45015eb9c803eebec154654895b0665e2..231d86a1dbde08d047b2a374bd091baa805e50c2 100644
--- a/Models/GraphEquivalence.v
+++ b/Models/GraphEquivalence.v
@@ -678,9 +678,20 @@ simpl activate. destruct_match_eq Hactive.
       simpl projT1. intro e.
       (* why does this stopped working between coq-8.16 and 8.19? *)
       (* cut ((bijectionG Ciso' (OnEdge e (1 /sr 2))) == (bijectionG (inverse Ciso) (OnEdge e (1 /sr 2)))). *)
-      cut (@equiv loc _ (bijectionG Ciso' (OnEdge e (1 /sr 2))) (bijectionG (inverse Ciso) (OnEdge e (1 /sr 2))));
-      try (now intros [Heq _]); [].
-      rewrite <- (HCf (OnEdge e (1 /sr 2))). reflexivity. }
+      pose (hsim := @bijectionG V E TG (inverse Ciso)).
+
+      assert (@equiv loc locG_Setoid
+                (@bijectionG V E TG Ciso' (@OnEdge V E TG e (1 /sr 2)))
+                (@hsim (@OnEdge V E TG e (1 /sr 2)) )).
+      { rewrite <- (HCf (OnEdge e (1 /sr 2))).
+        reflexivity. }
+      destruct H.
+      assumption.
+
+      (* cut (@equiv loc _ (bijectionG Ciso' (OnEdge e (1 /sr 2))) (bijectionG (inverse Ciso) (OnEdge e (1 /sr 2)))); *)
+      (* try (now intros [Heq _]); []. *)
+      (* rewrite <- (HCf (OnEdge e (1 /sr 2))). reflexivity. *)
+    }
     assert (HnotOnEdge : forall e p, Clocal_config (Good g) =/= SOnEdge e p).
     { intros e0 p0 H0.
       destruct (Clocal_config (Good g)) as [| e p] eqn:Habs; try tauto; [].
diff --git a/Spaces/Graph.v b/Spaces/Graph.v
index adcb662a6ad71f1c15a35d2d6545ccc1d52907a6..9ce11aa9a542f8dcc5dbd6043c801c013ebcedcc 100644
--- a/Spaces/Graph.v
+++ b/Spaces/Graph.v
@@ -17,24 +17,24 @@ Set Implicit Arguments.
 
 
 Class Graph (V E : Type) := {
-  V_Setoid :> Setoid V;
-  E_Setoid :> Setoid E;
-  V_EqDec :> EqDec V_Setoid;
-  E_EqDec :> EqDec E_Setoid;
+  #[global] V_Setoid :: Setoid V;
+  #[global] E_Setoid :: Setoid E;
+  #[global] V_EqDec :: EqDec V_Setoid;
+  #[global] E_EqDec :: EqDec E_Setoid;
 
   src : E -> V; (* source and target of an edge *)
   tgt : E -> V;
-  src_compat :> Proper (equiv ==> equiv) src;
-  tgt_compat :> Proper (equiv ==> equiv) tgt;
+  #[global] src_compat :: Proper (equiv ==> equiv) src;
+  #[global] tgt_compat :: Proper (equiv ==> equiv) tgt;
 
   find_edge : V -> V -> option E;
-  find_edge_compat :> Proper (equiv ==> equiv ==> opt_eq equiv) find_edge;
+  #[global] find_edge_compat :: Proper (equiv ==> equiv ==> opt_eq equiv) find_edge;
   find_edge_Some : ∀ e v1 v2, find_edge v1 v2 == Some e <-> v1 == src e /\ v2 == tgt e}.
 
 Class ThresholdGraph (V E : Type) := {
   nothreshold_graph : Graph V E;
   threshold : E -> strict_ratio;
-  threshold_compat :> Proper (equiv ==> equiv) threshold}.
+  #[global] threshold_compat :: Proper (equiv ==> equiv) threshold}.
 
 Coercion nothreshold_graph : ThresholdGraph >-> Graph.
 Global Existing Instance nothreshold_graph.
diff --git a/Util/FMaps/FMapInterface.v b/Util/FMaps/FMapInterface.v
index 96bb0e551f8b7bcbd435d050e02027c42c841929..ee95e963cb6421f8c07ccba3aea4c117d9f4535a 100644
--- a/Util/FMaps/FMapInterface.v
+++ b/Util/FMaps/FMapInterface.v
@@ -254,22 +254,22 @@ Class FMapSpecs_adjust `(FMap key) := {
 }. *)
 
 Class FMapSpecs `(F : FMap key) := {
-  FFMapSpecs_MapsTo :> FMapSpecs_MapsTo F;
-  FFMapSpecs_mem :> FMapSpecs_mem F;
-  FFMapSpecs_empty :> FMapSpecs_empty F;
-  FFMapSpecs_is_empty :> FMapSpecs_is_empty F;
-  FFMapSpecs_add :> FMapSpecs_add F;
-  FFMapSpecs_remove :> FMapSpecs_remove F;
-  FFMapSpecs_find :> FMapSpecs_find F;
-  FFMapSpecs_elements :> FMapSpecs_elements F;
-  FFMapSpecs_cardinal :> FMapSpecs_cardinal F;
-  FFMapSpecs_fold :> FMapSpecs_fold F;
-  FFMapSpecs_equal :> FMapSpecs_equal F;
-  FFMapSpecs_map :> FMapSpecs_map F;
-  FFMapSpecs_mapi :> FMapSpecs_mapi F;
-(*   FFMapSpecs_map2 :> FMapSpecs_map2 F; *)
-(*   FFMapSpecs_insert :> FMapSpecs_insert F; *)
-(*   FFMapSpecs_adjust :> FMapSpecs_adjust F *)
+  #[global] FFMapSpecs_MapsTo :: FMapSpecs_MapsTo F;
+  #[global] FFMapSpecs_mem :: FMapSpecs_mem F;
+  #[global] FFMapSpecs_empty :: FMapSpecs_empty F;
+  #[global] FFMapSpecs_is_empty :: FMapSpecs_is_empty F;
+  #[global] FFMapSpecs_add :: FMapSpecs_add F;
+  #[global] FFMapSpecs_remove :: FMapSpecs_remove F;
+  #[global] FFMapSpecs_find :: FMapSpecs_find F;
+  #[global] FFMapSpecs_elements :: FMapSpecs_elements F;
+  #[global] FFMapSpecs_cardinal :: FMapSpecs_cardinal F;
+  #[global] FFMapSpecs_fold :: FMapSpecs_fold F;
+  #[global] FFMapSpecs_equal :: FMapSpecs_equal F;
+  #[global] FFMapSpecs_map :: FMapSpecs_map F;
+  #[global] FFMapSpecs_mapi :: FMapSpecs_mapi F;
+(*   #[global] FFMapSpecs_map2 :: FMapSpecs_map2 F; *)
+(*   #[global] FFMapSpecs_insert :: FMapSpecs_insert F; *)
+(*   #[global] FFMapSpecs_adjust :: FMapSpecs_adjust F *)
 }.
 (* About Build_FMapSpecs. *)
 (* About FMapSpecs. *)
diff --git a/Util/FSets/FSetInterface.v b/Util/FSets/FSetInterface.v
index 758c0ba555393cc851c3db7635e705a8f00dc2b0..74e6c2a82516de8dd7c206bced633bd777d9f9c4 100644
--- a/Util/FSets/FSetInterface.v
+++ b/Util/FSets/FSetInterface.v
@@ -298,28 +298,28 @@ Class FSetSpecs_max_elt `(FSet A) := {
 }.*)
 
 Class FSetSpecs `(F : FSet A) := {
-  FFSetSpecs_In :> FSetSpecs_In F;
-  FFSetSpecs_mem :> FSetSpecs_mem F;
-  FFSetSpecs_equal :> FSetSpecs_equal F;
-  FFSetSpecs_subset :> FSetSpecs_subset F;
-  FFSetSpecs_empty :> FSetSpecs_empty F;
-  FFSetSpecs_is_empty :> FSetSpecs_is_empty F;
-  FFSetSpecs_add :> FSetSpecs_add F;
-  FFSetSpecs_remove :> FSetSpecs_remove F;
-  FFSetSpecs_singleton :> FSetSpecs_singleton F;
-  FFSetSpecs_union :> FSetSpecs_union F;
-  FFSetSpecs_inter :> FSetSpecs_inter F;
-  FFSetSpecs_diff :> FSetSpecs_diff F;
-  FFSetSpecs_fold :> FSetSpecs_fold F;
-  FFSetSpecs_cardinal :> FSetSpecs_cardinal F;
-  FFSetSpecs_filter :> FSetSpecs_filter F;
-  FFSetSpecs_for_all :> FSetSpecs_for_all F;
-  FFSetSpecs_exists :> FSetSpecs_exists F;
-  FFSetSpecs_partition :> FSetSpecs_partition F;
-  FFSetSpecs_elements :> FSetSpecs_elements F;
-  FFSetSpecs_choose :> FSetSpecs_choose F;
-  (* FFSetSpecs_min_elt :> FSetSpecs_min_elt F; *)
-  (* FFSetSpecs_max_elt :> FSetSpecs_max_elt F *)
+  #[global] FFSetSpecs_In :: FSetSpecs_In F;
+  #[global] FFSetSpecs_mem :: FSetSpecs_mem F;
+  #[global] FFSetSpecs_equal :: FSetSpecs_equal F;
+  FFSetSpecs_subset :: FSetSpecs_subset F;
+  #[global] FFSetSpecs_empty :: FSetSpecs_empty F;
+  #[global] FFSetSpecs_is_empty :: FSetSpecs_is_empty F;
+  #[global] FFSetSpecs_add :: FSetSpecs_add F;
+  #[global] FFSetSpecs_remove :: FSetSpecs_remove F;
+  #[global] FFSetSpecs_singleton :: FSetSpecs_singleton F;
+  #[global] FFSetSpecs_union :: FSetSpecs_union F;
+  #[global] FFSetSpecs_inter :: FSetSpecs_inter F;
+  #[global] FFSetSpecs_diff :: FSetSpecs_diff F;
+  #[global] FFSetSpecs_fold :: FSetSpecs_fold F;
+  #[global] FFSetSpecs_cardinal :: FSetSpecs_cardinal F;
+  #[global] FFSetSpecs_filter :: FSetSpecs_filter F;
+  #[global] FFSetSpecs_for_all :: FSetSpecs_for_all F;
+  #[global] FFSetSpecs_exists :: FSetSpecs_exists F;
+  #[global] FFSetSpecs_partition :: FSetSpecs_partition F;
+  #[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 *)
 }.
 (* About FSetSpecs. *)
 
diff --git a/Util/MMultiset/MMultisetInterface.v b/Util/MMultiset/MMultisetInterface.v
index 32734f148ee0e9c3d06054a92e5d521fbc92c5ec..de832e4136f1b8697068ac1f1ce35d0e0619df4a 100644
--- a/Util/MMultiset/MMultisetInterface.v
+++ b/Util/MMultiset/MMultisetInterface.v
@@ -230,22 +230,22 @@ Class SizeSpec elt `(FMOps elt) := {
 (** ***  Full specification  **)
 
 Class FMultisetsOn elt `(Ops : FMOps elt) := {
-  FullMultiplicitySpec :> MultiplicitySpec elt Ops;
-  FullEmptySpec :> EmptySpec elt Ops;
-  FullSingletonSpec :> SingletonSpec elt Ops;
-  FullAddSpec :> AddSpec elt Ops;
-  FullRemoveSpec :> RemoveSpec elt Ops;
-  FullBinarySpec :> BinarySpec elt Ops;
-  FullFoldSpec :> FoldSpec elt Ops;
-  FullTestSpec: > TestSpec elt Ops;
-  FullElementsSpec :> ElementsSpec elt Ops;
-  FullSupportSpec :> SupportSpec elt Ops;
-  FullChooseSpec :> ChooseSpec elt Ops;
-  FullPartitionSpec :> PartitionSpec elt Ops;
-  FullNpartitionSpec :> NpartitionSpec elt Ops;
-  FullQuantifierSpec :> QuantifierSpec elt Ops;
-  FullSizeSpec :> SizeSpec elt Ops;
-  FullFilterSpec :> FilterSpec elt Ops}.
+  #[global] FullMultiplicitySpec :: MultiplicitySpec elt Ops;
+  #[global] FullEmptySpec :: EmptySpec elt Ops;
+  #[global] FullSingletonSpec :: SingletonSpec elt Ops;
+  #[global] FullAddSpec :: AddSpec elt Ops;
+  #[global] FullRemoveSpec :: RemoveSpec elt Ops;
+  #[global] FullBinarySpec :: BinarySpec elt Ops;
+  #[global] FullFoldSpec :: FoldSpec elt Ops;
+  #[global] FullTestSpec :: TestSpec elt Ops;
+  #[global] FullElementsSpec :: ElementsSpec elt Ops;
+  #[global] FullSupportSpec :: SupportSpec elt Ops;
+  #[global] FullChooseSpec :: ChooseSpec elt Ops;
+  #[global] FullPartitionSpec :: PartitionSpec elt Ops;
+  #[global] FullNpartitionSpec :: NpartitionSpec elt Ops;
+  #[global] FullQuantifierSpec :: QuantifierSpec elt Ops;
+  #[global] FullSizeSpec :: SizeSpec elt Ops;
+  #[global] FullFilterSpec :: FilterSpec elt Ops}.
 
 
 (* Global Notation "s  [=]  t" := (eq s t) (at level 70, no associativity, only parsing). *)
diff --git a/Util/Preliminary.v b/Util/Preliminary.v
index 29c0edb23d0f91ebe5ddc2d28e59f5306d5616fd..0842f1c53153889cd350cdfb257d8e187fb9a3f6 100644
--- a/Util/Preliminary.v
+++ b/Util/Preliminary.v
@@ -93,9 +93,10 @@ Proof. intros ? ? Hneq ?. apply Hneq. now symmetry. Qed.
 Global Hint Extern 3 (relation_equivalence _ _) => symmetry : core.
 
 (** Notations for composition and inverse *)
+
 Class Composition T `{Setoid T} := {
   compose : T -> T -> T;
-  compose_compat :> Proper (equiv ==> equiv ==> equiv) compose }.
+  #[global]compose_compat :: Proper (equiv ==> equiv ==> equiv) compose }.
 Infix "∘" := compose (left associativity, at level 40).
 Arguments Composition T {_}.
 
@@ -103,7 +104,7 @@ Arguments Composition T {_}.
          (Bijection, Similarity, Isometry, etc.) *)
 Class Inverse T `{Setoid T} := {
   inverse : T -> T;
-  inverse_compat :> Proper (equiv ==> equiv) inverse }.
+  #[global]inverse_compat :: Proper (equiv ==> equiv) inverse }.
 Notation "bij ⁻¹" := (inverse bij) (at level 39).
 Arguments Inverse T {_}.