Remove undocumented Instance : ! syntax

It's used a few times in the stdlib (a couple of which need no other
change when removing the !) and not at all throughout our CI.

Considering that I think it's fair enough to remove it.

3 files changed, 6 insertions, 6 deletions

diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v
index c014ecc7ab..2dd254496b 100644
--- a/theories/Classes/CRelationClasses.v
+++ b/theories/Classes/CRelationClasses.v
@@ -337,7 +337,7 @@ Section Binary.
    morphism for equivalence (see Morphisms).  It is also sufficient to
    show that [R] is antisymmetric w.r.t. [eqA] *)
 
-  Global Instance partial_order_antisym `(PartialOrder eqA R) : ! Antisymmetric A eqA R.
+  Global Instance partial_order_antisym `(PartialOrder eqA R) : Antisymmetric eqA R.
   Proof with auto.
     reduce_goal.
     apply H. firstorder.
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index e9a9d6aff2..7f26181108 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -94,7 +94,7 @@ Program Instance unit_eqdec : EqDec unit eq := fun x y => in_left.
 Obligation Tactic := unfold complement, equiv ; program_simpl.
 
 Program Instance prod_eqdec `(EqDec A eq, EqDec B eq) :
-  ! EqDec (prod A B) eq :=
+  EqDec (prod A B) eq :=
   { equiv_dec x y :=
     let '(x1, x2) := x in
     let '(y1, y2) := y in
@@ -115,7 +115,7 @@ Program Instance sum_eqdec `(EqDec A eq, EqDec B eq) :
 (** Objects of function spaces with countable domains like bool have decidable
   equality. Proving the reflection requires functional extensionality though. *)
 
-Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq :=
+Program Instance bool_function_eqdec `(EqDec A eq) : EqDec (bool -> A) eq :=
   { equiv_dec f g :=
     if f true == g true then
       if f false == g false then in_left
@@ -130,7 +130,7 @@ Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq :=
 
 Require Import List.
 
-Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
+Program Instance list_eqdec `(eqa : EqDec A eq) : EqDec (list A) eq :=
   { equiv_dec :=
     fix aux (x y : list A) :=
     match x, y with
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 440b317573..3c0982cde7 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -464,7 +464,7 @@ Section Binary.
    morphism for equivalence (see Morphisms).  It is also sufficient to
    show that [R] is antisymmetric w.r.t. [eqA] *)
 
-  Global Instance partial_order_antisym `(PartialOrder eqA R) : ! Antisymmetric A eqA R.
+  Global Instance partial_order_antisym `(PartialOrder eqA R) : Antisymmetric A eqA R.
   Proof with auto.
     reduce_goal.
     pose proof partial_order_equivalence as poe. do 3 red in poe.
@@ -481,7 +481,7 @@ Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : type
 (** The partial order defined by subrelation and relation equivalence. *)
 
 Program Instance subrelation_partial_order :
-  ! PartialOrder (relation A) relation_equivalence subrelation.
+  PartialOrder (@relation_equivalence A) subrelation.
 
 Next Obligation.
 Proof.