Default disable automatic generalization of Instance type

Fix #6042

Also introduce a deprecated compat option

5 files changed, 32 insertions, 34 deletions

diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 9a3a1d3709..aae24e0e0a 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -1,4 +1,4 @@
-(* -*- coding: utf-8; coq-prog-args: ("-coqlib" "../.." "-R" ".." "Coq" "-top" "Coq.Classes.CMorphisms") -*- *)
+(* -*- coding: utf-8; coq-prog-args: ("-top" "Coq.Classes.CMorphisms") -*- *)
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
 (*  v      *         Copyright INRIA, CNRS and contributors             *)
@@ -308,7 +308,7 @@ Section GenericInstances.
 
   Global Program 
   Instance trans_contra_inv_impl_type_morphism
-  `(Transitive A R) : Proper (R --> flip arrow) (R x) | 3.
+  `(Transitive A R) {x} : Proper (R --> flip arrow) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -318,7 +318,7 @@ Section GenericInstances.
 
   Global Program 
   Instance trans_co_impl_type_morphism
-    `(Transitive A R) : Proper (R ++> arrow) (R x) | 3.
+    `(Transitive A R) {x} : Proper (R ++> arrow) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -328,7 +328,7 @@ Section GenericInstances.
 
   Global Program 
   Instance trans_sym_co_inv_impl_type_morphism
-    `(PER A R) : Proper (R ++> flip arrow) (R x) | 3.
+    `(PER A R) {x} : Proper (R ++> flip arrow) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -337,7 +337,7 @@ Section GenericInstances.
   Qed.
 
   Global Program Instance trans_sym_contra_arrow_morphism
-    `(PER A R) : Proper (R --> arrow) (R x) | 3.
+    `(PER A R) {x} : Proper (R --> arrow) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -346,7 +346,7 @@ Section GenericInstances.
   Qed.
 
   Global Program Instance per_partial_app_type_morphism
-  `(PER A R) : Proper (R ==> iffT) (R x) | 2.
+  `(PER A R) {x} : Proper (R ==> iffT) (R x) | 2.
 
   Next Obligation.
   Proof with auto.
@@ -399,17 +399,17 @@ Section GenericInstances.
   (** Coq functions are morphisms for Leibniz equality,
      applied only if really needed. *)
 
-  Global Instance reflexive_eq_dom_reflexive `(Reflexive B R') :
+  Global Instance reflexive_eq_dom_reflexive `(Reflexive B R') {A} :
     Reflexive (@Logic.eq A ==> R').
   Proof. simpl_crelation. Qed.
 
   (** [respectful] is a morphism for crelation equivalence . *)
 
-  Global Instance respectful_morphism :
+  Global Instance respectful_morphism {A B} :
     Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) 
            (@respectful A B).
   Proof. 
-    intros A B R R' HRR' S S' HSS' f g. 
+    intros R R' HRR' S S' HSS' f g.
     unfold respectful , relation_equivalence in *; simpl in *.
     split ; intros H x y Hxy.
     - apply (fst (HSS' _ _)). apply H. now apply (snd (HRR' _ _)).
@@ -511,9 +511,9 @@ Ltac partial_application_tactic :=
 
 (** Bootstrap !!! *)
 
-Instance proper_proper : Proper (relation_equivalence ==> eq ==> iffT) (@Proper A).
+Instance proper_proper {A} : Proper (relation_equivalence ==> eq ==> iffT) (@Proper A).
 Proof.
-  intros A R R' HRR' x y <-. red in HRR'.
+  intros R R' HRR' x y <-. red in HRR'.
   split ; red ; intros. 
   - now apply (fst (HRR' _ _)).
   - now apply (snd (HRR' _ _)).
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index c70e3fe478..867d9cb9b3 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,4 +1,4 @@
-(* -*- coding: utf-8; coq-prog-args: ("-coqlib" "../.." "-R" ".." "Coq" "-top" "Coq.Classes.Morphisms") -*- *)
+(* -*- coding: utf-8; coq-prog-args: ("-top" "Coq.Classes.Morphisms") -*- *)
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
 (*  v      *         Copyright INRIA, CNRS and contributors             *)
@@ -309,7 +309,7 @@ Section GenericInstances.
 
   Global Program 
   Instance trans_contra_inv_impl_morphism
-  `(Transitive A R) : Proper (R --> flip impl) (R x) | 3.
+  `(Transitive A R) {x} : Proper (R --> flip impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -319,7 +319,7 @@ Section GenericInstances.
 
   Global Program 
   Instance trans_co_impl_morphism
-    `(Transitive A R) : Proper (R ++> impl) (R x) | 3.
+    `(Transitive A R) {x} : Proper (R ++> impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -329,7 +329,7 @@ Section GenericInstances.
 
   Global Program 
   Instance trans_sym_co_inv_impl_morphism
-    `(PER A R) : Proper (R ++> flip impl) (R x) | 3.
+    `(PER A R) {x} : Proper (R ++> flip impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -338,7 +338,7 @@ Section GenericInstances.
   Qed.
 
   Global Program Instance trans_sym_contra_impl_morphism
-    `(PER A R) : Proper (R --> impl) (R x) | 3.
+    `(PER A R) {x} : Proper (R --> impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -347,7 +347,7 @@ Section GenericInstances.
   Qed.
 
   Global Program Instance per_partial_app_morphism
-  `(PER A R) : Proper (R ==> iff) (R x) | 2.
+  `(PER A R) {x} : Proper (R ==> iff) (R x) | 2.
 
   Next Obligation.
   Proof with auto.
@@ -520,9 +520,9 @@ Ltac partial_application_tactic :=
 
 (** Bootstrap !!! *)
 
-Instance proper_proper : Proper (relation_equivalence ==> eq ==> iff) (@Proper A).
+Instance proper_proper {A} : Proper (relation_equivalence ==> eq ==> iff) (@Proper A).
 Proof.
-  intros A x y H y0 y1 e; destruct e.
+  intros x y H y0 y1 e; destruct e.
   reduce in H.
   split ; red ; intros H0.
   - setoid_rewrite <- H.
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index a168a8e7cd..964786d8e6 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -22,11 +22,11 @@ Generalizable Variables A l.
 
 (** Morphisms for relations *)
 
-Instance relation_conjunction_morphism : Proper (relation_equivalence (A:=A) ==>
+Instance relation_conjunction_morphism {A} : Proper (relation_equivalence (A:=A) ==>
   relation_equivalence ==> relation_equivalence) relation_conjunction.
   Proof. firstorder. Qed.
 
-Instance relation_disjunction_morphism : Proper (relation_equivalence (A:=A) ==>
+Instance relation_disjunction_morphism {A} : Proper (relation_equivalence (A:=A) ==>
   relation_equivalence ==> relation_equivalence) relation_disjunction.
   Proof. firstorder. Qed.
 
@@ -43,11 +43,11 @@ Proof. do 2 red. unfold predicate_implication. auto. Qed.
 (** The instantiation at relation allows rewriting applications of relations
     [R x y] to [R' x y]  when [R] and [R'] are in [relation_equivalence]. *)
 
-Instance relation_equivalence_pointwise :
+Instance relation_equivalence_pointwise {A} :
   Proper (relation_equivalence ==> pointwise_relation A (pointwise_relation A iff)) id.
 Proof. intro. apply (predicate_equivalence_pointwise (Tcons A (Tcons A Tnil))). Qed.
 
-Instance subrelation_pointwise :
+Instance subrelation_pointwise {A} :
   Proper (subrelation ==> pointwise_relation A (pointwise_relation A impl)) id.
 Proof. intro. apply (predicate_implication_pointwise (Tcons A (Tcons A Tnil))). Qed.
 
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 5381e91997..401d7007e2 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -395,7 +395,7 @@ Notation "∙⊥∙" := false_predicate : predicate_scope.
 
 (** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *)
 
-Program Instance predicate_equivalence_equivalence : 
+Program Instance predicate_equivalence_equivalence {l} :
   Equivalence (@predicate_equivalence l).
 
   Next Obligation.
@@ -413,7 +413,7 @@ Program Instance predicate_equivalence_equivalence :
       firstorder.
   Qed.
 
-Program Instance predicate_implication_preorder :
+Program Instance predicate_implication_preorder {l} :
   PreOrder (@predicate_implication l).
   Next Obligation.
     intro l; induction l ; firstorder.
@@ -480,7 +480,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 :
+Program Instance subrelation_partial_order {A} :
   PartialOrder (@relation_equivalence A) subrelation.
 
 Next Obligation.
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index b4034b9cf9..09c25b38a6 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -61,11 +61,9 @@ Class Measure {A B} (f : A -> B).
 
 (** Standard measures. *)
 
-Instance fst_measure : @Measure (A * B) A Fst.
-Defined.
+Instance fst_measure {A B} : @Measure (A * B) A Fst := {}.
 
-Instance snd_measure : @Measure (A * B) B Snd.
-Defined.
+Instance snd_measure {A B} : @Measure (A * B) B Snd := {}.
 
 (** We define a product relation over [A*B]: each components should
     satisfy the corresponding initial relation. *)
@@ -96,11 +94,11 @@ Section RelCompFun_Instances.
     `(Measure A B f, Irreflexive _ R) : Irreflexive (R@@f).
   Proof. firstorder. Qed.
 
-  Global Program Instance RelCompFun_Equivalence
-    `(Measure A B f, Equivalence _ R) : Equivalence (R@@f).
+  Global Instance RelCompFun_Equivalence
+    `(Measure A B f, Equivalence _ R) : Equivalence (R@@f) := {}.
 
-  Global Program Instance RelCompFun_StrictOrder
-    `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f).
+  Global Instance RelCompFun_StrictOrder
+    `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f) := {}.
 
 End RelCompFun_Instances.