Add the ability to specify what to do with free variables in instance

declarations. By default, print the list of implicitely generalized
variables. Implement new commands Add Parametric Relation/Morphism for...
parametric relations and morphisms. Now the Add * commands are strict
about free vars and will fail if there remain some. Parametric just allows to
give a variable context. Also, correct a bug in generalization of
implicits that ordered the variables in the wrong order.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10782 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 29 insertions, 30 deletions

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 975dcf1dd0..552ff996ae 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -128,9 +128,9 @@ Proof. firstorder. Qed.
 Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl).
 Proof. firstorder. Qed.
 
-Instance [ subrelation A R R' ] => pointwise_subrelation :
+Instance [ sub : subrelation A R R' ] => pointwise_subrelation :
   subrelation (pointwise_relation (A:=B) R) (pointwise_relation R') | 4.
-Proof. reduce. unfold pointwise_relation in *. apply subrelation0. apply H. Qed.
+Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed.
 
 (** The complement of a relation conserves its morphisms. *)
 
@@ -186,7 +186,7 @@ Program Instance [ Transitive A R ] =>
 
 (** Morphism declarations for partial applications. *)
 
-Program Instance [ Transitive A R ] (x : A) =>
+Program Instance [ Transitive A R ] =>
   trans_contra_inv_impl_morphism : Morphism (R --> inverse impl) (R x).
 
   Next Obligation.
@@ -194,7 +194,7 @@ Program Instance [ Transitive A R ] (x : A) =>
     transitivity y...
   Qed.
 
-Program Instance [ Transitive A R ] (x : A) =>
+Program Instance [ Transitive A R ] =>
   trans_co_impl_morphism : Morphism (R ==> impl) (R x).
 
   Next Obligation.
@@ -202,7 +202,7 @@ Program Instance [ Transitive A R ] (x : A) =>
     transitivity x0...
   Qed.
 
-Program Instance [ Transitive A R, Symmetric A R ] (x : A) =>
+Program Instance [ Transitive A R, Symmetric A R ] =>
   trans_sym_co_inv_impl_morphism : Morphism (R ==> inverse impl) (R x).
 
   Next Obligation.
@@ -210,7 +210,7 @@ Program Instance [ Transitive A R, Symmetric A R ] (x : A) =>
     transitivity y...
   Qed.
 
-Program Instance [ Transitive A R, Symmetric _ R ] (x : A) =>
+Program Instance [ Transitive A R, Symmetric _ R ] =>
   trans_sym_contra_impl_morphism : Morphism (R --> impl) (R x).
 
   Next Obligation.
@@ -218,7 +218,7 @@ Program Instance [ Transitive A R, Symmetric _ R ] (x : A) =>
     transitivity x0...
   Qed.
 
-Program Instance [ Equivalence A R ] (x : A) =>
+Program Instance [ Equivalence A R ] =>
   equivalence_partial_app_morphism : Morphism (R ==> iff) (R x).
 
   Next Obligation.
@@ -231,7 +231,7 @@ Program Instance [ Equivalence A R ] (x : A) =>
 
 (** [R] is Reflexive, hence we can build the needed proof. *)
 
-Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive _ R ] (x : A) =>
+Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive _ R ]  =>
   Reflexive_partial_app_morphism : Morphism R' (m x) | 4.
 
 (** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof
@@ -294,7 +294,7 @@ Program Instance inverse_iff_impl_id :
 (** Coq functions are morphisms for leibniz equality, 
    applied only if really needed. *)
 
-Instance (A : Type) [ Reflexive B R ] (m : A -> B) =>
+Instance (A : Type) [ Reflexive B R ] =>
   eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3.
 Proof. simpl_relation. Qed.
 
@@ -305,7 +305,7 @@ Proof. simpl_relation. Qed.
 (** [respectful] is a morphism for relation equivalence. *)
 
 Instance respectful_morphism : 
-  Morphism (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). 
+  Morphism (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B).
 Proof.
   reduce.
   unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *.
@@ -335,14 +335,14 @@ Qed.
 Class (A : Type) => Normalizes (m : relation A) (m' : relation A) : Prop :=
   normalizes : relation_equivalence m m'.
 
-Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) =>
-  inverse_respectful_norm : Normalizes _ (inverse R ==> inverse R') (inverse (R ==> R')) .
+Instance inverse_respectful_norm : 
+  Normalizes (A -> B) (inverse R ==> inverse R') (inverse (R ==> R')) .
 Proof. firstorder. Qed.
 
 (* If not an inverse on the left, do a double inverse. *)
 
-Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) =>
-  not_inverse_respectful_norm : Normalizes _ (R ==> inverse R') (inverse (inverse R ==> R')) | 4.
+Instance not_inverse_respectful_norm : 
+  Normalizes (A -> B) (R ==> inverse R') (inverse (inverse R ==> R')) | 4.
 Proof. firstorder. Qed.
 
 Instance [ Normalizes B R' (inverse R'') ] =>
@@ -391,4 +391,3 @@ Ltac morphism_normalization :=
   end.
 
 Hint Extern 5 (@Morphism _ _ _) => morphism_normalization : typeclass_instances.
-
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index f7f460123e..526264612f 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -131,7 +131,7 @@ Implicit Arguments setoid_morphism [[!sa]].
 Existing Instance setoid_morphism.
 
 Program Definition setoid_partial_app_morphism [ sa : Setoid A ] (x : A) : Morphism (equiv ++> iff) (equiv x) :=
-  Reflexive_partial_app_morphism x.
+  Reflexive_partial_app_morphism.
 
 Existing Instance setoid_partial_app_morphism.
 
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 617ea6f4f6..e033343d1d 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -662,19 +662,19 @@ Add Relation key E.eq
 
 Implicit Arguments Equal [[elt]].
 
-Add Relation (t elt) Equal  
+Add Parametric Relation (elt : Type) : (t elt) Equal  
  reflexivity proved by (@Equal_refl elt)
  symmetry proved by (@Equal_sym elt)
  transitivity proved by (@Equal_trans elt)
  as EqualSetoid.
 
-Add Morphism (@In elt) with signature E.eq ==> Equal ==> iff as In_m.
+Add Parametric Morphism elt : (@In elt) with signature E.eq ==> Equal ==> iff as In_m.
 Proof.
 unfold Equal; intros k k' Hk m m' Hm.
 rewrite (In_iff m Hk), in_find_iff, in_find_iff, Hm; intuition.
 Qed.
 
-Add Morphism (@MapsTo elt)
+Add Parametric Morphism elt : (@MapsTo elt)
  with signature E.eq ==> @Logic.eq _ ==> Equal ==> iff as MapsTo_m.
 Proof.
 unfold Equal; intros k k' Hk e m m' Hm.
@@ -682,26 +682,26 @@ rewrite (MapsTo_iff m e Hk), find_mapsto_iff, find_mapsto_iff, Hm;
  intuition.
 Qed.
 
-Add Morphism (@Empty elt) with signature Equal ==> iff as Empty_m.
+Add Parametric Morphism elt : (@Empty elt) with signature Equal ==> iff as Empty_m.
 Proof.
 unfold Empty; intros m m' Hm; intuition.
 rewrite <-Hm in H0; eauto.
 rewrite Hm in H0; eauto.
 Qed.
 
-Add Morphism (@is_empty elt) with signature Equal ==> @Logic.eq _ as is_empty_m.
+Add Parametric Morphism elt : (@is_empty elt) with signature Equal ==> @Logic.eq _ as is_empty_m.
 Proof.
 intros m m' Hm.
 rewrite eq_bool_alt, <-is_empty_iff, <-is_empty_iff, Hm; intuition.
 Qed.
 
-Add Morphism (@mem elt) with signature E.eq ==> Equal ==> @Logic.eq _ as mem_m.
+Add Parametric Morphism elt : (@mem elt) with signature E.eq ==> Equal ==> @Logic.eq _ as mem_m.
 Proof.
 intros k k' Hk m m' Hm.
 rewrite eq_bool_alt, <- mem_in_iff, <-mem_in_iff, Hk, Hm; intuition.
 Qed.
 
-Add Morphism (@find elt) with signature E.eq ==> Equal ==> @Logic.eq _ as find_m.
+Add Parametric Morphism elt : (@find elt) with signature E.eq ==> Equal ==> @Logic.eq _ as find_m.
 Proof.
 intros k k' Hk m m' Hm.
 generalize (find_mapsto_iff m k)(find_mapsto_iff m' k')
@@ -712,7 +712,7 @@ rewrite <- H1, Hk, Hm, H2; auto.
 symmetry; rewrite <- H2, <-Hk, <-Hm, H1; auto.
 Qed.
 
-Add Morphism (@add elt) with signature 
+Add Parametric Morphism elt : (@add elt) with signature 
  E.eq ==> @Logic.eq _ ==> Equal ==> Equal as add_m.
 Proof.
 intros k k' Hk e m m' Hm y.
@@ -721,7 +721,7 @@ elim n; rewrite <-Hk; auto.
 elim n; rewrite Hk; auto.
 Qed.
 
-Add Morphism (@remove elt) with signature
+Add Parametric Morphism elt : (@remove elt) with signature
  E.eq ==> Equal ==> Equal as remove_m.
 Proof.
 intros k k' Hk m m' Hm y.
@@ -730,7 +730,7 @@ elim n; rewrite <-Hk; auto.
 elim n; rewrite Hk; auto.
 Qed.
 
-Add Morphism (@map elt elt') with signature @Logic.eq _ ==> Equal ==> Equal as map_m.
+Add Parametric Morphism elt elt' : (@map elt elt') with signature @Logic.eq _ ==> Equal ==> Equal as map_m.
 Proof.
 intros f m m' Hm y.
 rewrite map_o, map_o, Hm; auto.
@@ -1104,7 +1104,7 @@ Module WProperties (E:DecidableType)(M:WSfun E).
 
  End Elt.
 
- Add Morphism (@cardinal elt) with signature Equal ==> @Logic.eq _ as cardinal_m.
+ Add Parametric Morphism elt : (@cardinal elt) with signature Equal ==> @Logic.eq _ as cardinal_m.
  Proof. intros; apply Equal_cardinal; auto. Qed.
 
 End WProperties.
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index fc2cc81ebd..1a11f7a131 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -81,7 +81,7 @@ function (by recursion) that maps 0 to false and the successor to true *)
 Definition if_zero (A : Set) (a b : A) (n : N) : A :=
   recursion a (fun _ _ => b) n.
 
-Add Morphism (if_zero A) with signature ((@eq (A:Set)) ==> (@eq A) ==> Neq ==> (@eq A)) as if_zero_wd.
+Add Parametric Morphism (A : Set) : (if_zero A) with signature (@eq _ ==> @eq _ ==> Neq ==> @eq _) as if_zero_wd.
 Proof.
 intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)).
 reflexivity. unfold fun2_eq; now intros. assumption.
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index c063c7bc1d..f042ab0685 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -148,13 +148,13 @@ intros R1 R2 R3 H1 H2 x y; rewrite H1; apply H2.
 now symmetry.
 Qed.
 
-Add Relation (A -> B -> Prop) (@relations_eq A B)
+Add Parametric Relation (A B : Type) : (A -> B -> Prop) (@relations_eq A B)
   reflexivity proved by (proj1 (relations_eq_equiv A B))
   symmetry proved by (proj2 (proj2 (relations_eq_equiv A B)))
   transitivity proved by (proj1 (proj2 (relations_eq_equiv A B)))
 as relations_eq_rel.
 
-Add Morphism (@well_founded A) with signature (@relations_eq A A) ==> iff as well_founded_wd.
+Add Parametric Morphism (A : Type) : (@well_founded A) with signature (@relations_eq A A) ==> iff as well_founded_wd.
 Proof.
 unfold relations_eq, well_founded; intros R1 R2 H;
 split; intros H1 a; induction (H1 a) as [x H2 H3]; constructor;