diff --git a/src/Common.v b/src/Common.v
index e3ea01bf..758fac87 100644
--- a/src/Common.v
+++ b/src/Common.v
@@ -479,8 +479,10 @@ Class ReflexiveT A (R : A -> A -> Type) :=
 Class TransitiveT A (R : A -> A -> Type) :=
   transitivityT : forall x y z, R x y -> R y z -> R x z.
 Class PreOrderT A (R : A -> A -> Type) :=
-  { PreOrderT_ReflexiveT :> ReflexiveT R;
-    PreOrderT_TransitiveT :> TransitiveT R }.
+  { PreOrderT_ReflexiveT : ReflexiveT R;
+    PreOrderT_TransitiveT : TransitiveT R }.
+#[global] Existing Instance PreOrderT_ReflexiveT.
+#[global] Existing Instance PreOrderT_TransitiveT.
 Definition respectful_heteroT A B C D
            (R : A -> B -> Type)
            (R' : forall (x : A) (y : B), C x -> D y -> Type)
diff --git a/src/Common/Frame.v b/src/Common/Frame.v
index 65681af9..565e216c 100644
--- a/src/Common/Frame.v
+++ b/src/Common/Frame.v
@@ -283,10 +283,11 @@ Arguments PreO.max {A} {le} _ _ _.
     such that [eq x y] exactly when both [le x y] and [le y x]. *)
 Module PO.
   Class t {A : Type} {le : A -> A -> Prop} {eq : A -> A -> Prop} : Prop :=
-    { PreO :> PreO.t le
+    { PreO : PreO.t le
       ; le_proper : Proper (eq ==> eq ==> iff) le
       ; le_antisym : forall x y, le x y -> le y x -> eq x y
     }.
+  #[global] Existing Instance PreO.
 
   Arguments t {A} le eq.
 
@@ -494,10 +495,11 @@ Module JoinLat.
       a join semi-lattice? We need [le] and [eq] to be a partial order,
       and we need our [max] operation to actually implement a maximum. *)
   Class t {A : Type} {O : Ops A} : Prop :=
-    { PO :> PO.t le eq
+    { PO : PO.t le eq
       ; max_proper : Proper (eq ==> eq ==> eq) max
       ; max_ok : forall l r, PreO.max (le := le) l r (max l r)
     }.
+  #[global] Existing Instance PO.
 
   Arguments t : clear implicits.
 
@@ -670,10 +672,11 @@ Module MeetLat.
   Arguments Ops : clear implicits.
 
   Class t {A : Type} {O : Ops A} : Prop :=
-    { PO :> PO.t le eq
+    { PO : PO.t le eq
       ; min_proper : Proper (eq ==> eq ==> eq) min
       ; min_ok : forall l r, PreO.min (le := le) l r (min l r)
     }.
+  #[global] Existing Instance PO.
 
   Arguments t : clear implicits.
 
@@ -866,12 +869,13 @@ Module Lattice.
   Arguments Ops : clear implicits.
 
   Class t {A : Type} {O : Ops A} : Prop :=
-    { PO :> PO.t le eq
+    { PO : PO.t le eq
       ; max_proper : Proper (eq ==> eq ==> eq) max
       ; max_ok : forall l r, PreO.max (le := le) l r (max l r)
       ; min_proper : Proper (eq ==> eq ==> eq) min
       ; min_ok : forall l r, PreO.min (le := le) l r (min l r)
     }.
+  #[global] Existing Instance PO.
 
   Arguments t : clear implicits.
 
@@ -1257,20 +1261,22 @@ End CompleteLattice.
  *)
 Module Frame.
   Class Ops {A} :=
-    { LOps :> L.Ops A
+    { LOps : L.Ops A
       ; sup : forall {Ix : Type}, (Ix -> A) -> A
     }.
+  #[global] Existing Instance LOps.
 
   Arguments Ops : clear implicits.
 
   Class t {A} {OA : Ops A}: Type :=
-    { L :> L.t A LOps
+    { L : L.t A LOps
       ; sup_proper : forall {Ix : Type},
           Proper (pointwise_relation _ L.eq ==> L.eq) (@sup _ _ Ix)
       ; sup_ok :  forall {Ix : Type} (f : Ix -> A), PreO.sup (le := L.le) f (sup f)
       ; sup_distr : forall x {Ix : Type} (f : Ix -> A)
         , L.eq (L.min x (sup f)) (sup (fun i => L.min x (f i)))
     }.
+  #[global] Existing Instance L.
 
   Arguments t : clear implicits.
   Section Facts.
@@ -1489,12 +1495,14 @@ Module CommIdemSG.
   (** [dot] is a binary operation which is commutative, idempotent, and
     associative. It is effectively a max or min. *)
   Class t {A} {eq : A -> A -> Prop} {dot : A -> A -> A} :=
-    { eq_equiv :> Equivalence eq
-      ; dot_proper :> Proper (eq ==> eq ==> eq) dot
+    { eq_equiv : Equivalence eq
+      ; dot_proper : Proper (eq ==> eq ==> eq) dot
       ; dot_idempotent : forall a, eq (dot a a) a
       ; dot_comm : forall a b, eq (dot a b) (dot b a)
       ; dot_assoc : forall a b c, eq (dot a (dot b c)) (dot (dot a b) c)
     }.
+  #[global] Existing Instance eq_equiv.
+  #[global] Existing Instance dot_proper.
 
   Arguments t : clear implicits.
 
diff --git a/src/Common/Gensym.v b/src/Common/Gensym.v
index d29755af..1eaeb18d 100644
--- a/src/Common/Gensym.v
+++ b/src/Common/Gensym.v
@@ -11,10 +11,12 @@ Class PreGensym A :=
   { s_gt : A -> A -> Prop;
     sym_init : A;
     combine_symbols : A -> A -> A;
-    s_gt_Asymmetric :> Asymmetric s_gt;
-    s_gt_Transitive :> Transitive s_gt;
+    s_gt_Asymmetric : Asymmetric s_gt;
+    s_gt_Transitive : Transitive s_gt;
     combine_respectful_l : forall x y, s_gt (combine_symbols x y) x;
     combine_respectful_r : forall x y, s_gt (combine_symbols x y) y }.
+  #[global] Existing Instance s_gt_Asymmetric.
+  #[global] Existing Instance s_gt_Transitive.
 
 Delimit Scope gensym_scope with gensym.
 Infix ">" := s_gt : gensym_scope.
diff --git a/src/Common/Monad.v b/src/Common/Monad.v
index 0b1c2952..1f0c575b 100644
--- a/src/Common/Monad.v
+++ b/src/Common/Monad.v
@@ -26,14 +26,16 @@ Class MonadLaws M `{MonadOps M}
 Arguments MonadLaws M {_}.
 
 Class MonadTransformerOps (T : (Type -> Type) -> (Type -> Type))
-  := { Tops :> forall M `{MonadOps M}, MonadOps (T M);
+  := { Tops : forall M `{MonadOps M}, MonadOps (T M);
        lift : forall {M} `{MonadOps M} {A}, M A -> T M A }.
+#[global] Existing Instance Tops.
 
 Class MonadTransformerLaws T `{MonadTransformerOps T}
-  := { Tlaws :> forall {M} `{MonadLaws M}, MonadLaws (T M);
+  := { Tlaws : forall {M} `{MonadLaws M}, MonadLaws (T M);
        lift_ret : forall {M} `{MonadLaws M} {A} (x : A), lift (ret x) = ret x;
        lift_bind : forall {M} `{MonadLaws M} {A B} (f : A -> M B) x,
                      lift (bind x f) = bind (lift x) (fun u => lift (f u)) }.
+#[global] Existing Instance Tlaws.
 Arguments MonadTransformerLaws T {_}.
 
 Create HintDb monad discriminated.
diff --git a/src/Parsers/ContextFreeGrammar/Fix/Definitions.v b/src/Parsers/ContextFreeGrammar/Fix/Definitions.v
index ee64a268..eef0c1f7 100644
--- a/src/Parsers/ContextFreeGrammar/Fix/Definitions.v
+++ b/src/Parsers/ContextFreeGrammar/Fix/Definitions.v
@@ -156,7 +156,7 @@ Proof.
 Qed.
 
 Class grammar_fixedpoint_lattice_data prestate :=
-  { state :> _ := lattice_for prestate;
+  { state : _ := lattice_for prestate;
     prestate_lt : prestate -> prestate -> bool;
     state_lt : state -> state -> bool
     := lattice_for_lt prestate_lt;
diff --git a/src/Parsers/ContextFreeGrammar/Fold.v b/src/Parsers/ContextFreeGrammar/Fold.v
index 7c7c6a65..1d9824df 100644
--- a/src/Parsers/ContextFreeGrammar/Fold.v
+++ b/src/Parsers/ContextFreeGrammar/Fold.v
@@ -168,7 +168,7 @@ Section fold_correctness.
       Ppat : nonterminals_listT -> production Char -> T -> Type;
       Ppats : nonterminals_listT -> productions Char -> T -> Type }.
   Class fold_grammar_correctness_data :=
-    { fgccd :> fold_grammar_correctness_computational_data;
+    { fgccd : fold_grammar_correctness_computational_data;
       Pnt_lift : forall valid0 nt value,
                    sub_nonterminals_listT valid0 initial_nonterminals_data
                    -> is_valid_nonterminal valid0 (of_nonterminal nt)
@@ -198,6 +198,7 @@ Section fold_correctness.
                      -> Ppat valid0 x p
                      -> Ppats valid0 xs ps
                      -> Ppats valid0 (x::xs) (combine_productions p ps) }.
+  #[global] Existing Instance fgccd.
   Context {FGCD : fold_grammar_correctness_data}.
 
   Lemma fold_production'_correct
diff --git a/src/Parsers/CorrectnessBaseTypes.v b/src/Parsers/CorrectnessBaseTypes.v
index ad93a835..a0054ceb 100644
--- a/src/Parsers/CorrectnessBaseTypes.v
+++ b/src/Parsers/CorrectnessBaseTypes.v
@@ -46,7 +46,10 @@ Section general.
       : split_list_completeT split_string_for_production }.
 
   Class boolean_parser_correctness_dataT :=
-    { data :> boolean_parser_dataT;
-      rdata' :> @parser_removal_dataT' _ G _;
-      cdata' :> boolean_parser_completeness_dataT' }.
+    { data : boolean_parser_dataT;
+      rdata' : @parser_removal_dataT' _ G _;
+      cdata' : boolean_parser_completeness_dataT' }.
+  #[global] Existing Instance data.
+  #[global] Existing Instance rdata'.
+  #[global] Existing Instance cdata'.
 End general.
diff --git a/src/Parsers/StringLike/Core.v b/src/Parsers/StringLike/Core.v
index 676b526e..f3fc319f 100644
--- a/src/Parsers/StringLike/Core.v
+++ b/src/Parsers/StringLike/Core.v
@@ -20,7 +20,7 @@ Reserved Notation "[ x ]".
 Module Export StringLike.
   Class StringLikeMin {Char : Type} :=
     {
-      String :> Type;
+      String : Type;
       char_at_matches : nat -> String -> (Char -> bool) -> bool;
       unsafe_get : nat -> String -> Char;
       length : String -> nat
@@ -114,11 +114,11 @@ Module Export StringLike.
       unsafe_get_correct : forall n s ch, get n s = Some ch -> unsafe_get n s = ch;
       length_singleton : forall s ch, s ~= [ ch ] -> length s = 1;
       bool_eq_char : forall s s' ch, s ~= [ ch ] -> s' ~= [ ch ] -> s =s s';
-      is_char_Proper :> Proper (beq ==> eq ==> eq) is_char;
-      length_Proper :> Proper (beq ==> eq) length;
-      take_Proper :> Proper (eq ==> beq ==> beq) take;
-      drop_Proper :> Proper (eq ==> beq ==> beq) drop;
-      bool_eq_Equivalence :> Equivalence beq;
+      is_char_Proper : Proper (beq ==> eq ==> eq) is_char;
+      length_Proper : Proper (beq ==> eq) length;
+      take_Proper : Proper (eq ==> beq ==> beq) take;
+      drop_Proper : Proper (eq ==> beq ==> beq) drop;
+      bool_eq_Equivalence : Equivalence beq;
       bool_eq_empty : forall str str', length str = 0 -> length str' = 0 -> str =s str';
       take_short_length : forall str n, n <= length str -> length (take n str) = n;
       take_long : forall str n, length str <= n -> take n str =s str;
@@ -131,6 +131,11 @@ Module Export StringLike.
       bool_eq_from_get : forall str str', (forall n, get n str = get n str') -> str =s str';
       strings_nontrivial : forall n, exists str, length str = n
     }.
+  #[global] Existing Instance is_char_Proper.
+  #[global] Existing Instance length_Proper.
+  #[global] Existing Instance take_Proper.
+  #[global] Existing Instance drop_Proper.
+  #[global] Existing Instance bool_eq_Equivalence.
 
   Class StringIsoProperties {Char} {HSLM} {HSL : @StringLike Char HSLM} {HSI : @StringIso Char HSLM} :=
     {