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

2 files changed, 3 insertions, 3 deletions

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;