Fix a bug found by B. Grégoire when declaring morphisms in module

types. Change (again) the semantics of bindings and the binding modifier
! in typeclasses. Inside [ ], implicit binding where only parameters
need to be given is the default, use ! to use explicit binding, which is
equivalent to regular bindings except for generalization of free
variables. Outside brackets (e.g. on the right of instance
declarations),  explicit binding is the default, and implicit binding
can be used by adding ! in front. This avoids almost every use of ! in
the standard library and in other examples I have.


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

5 files changed, 60 insertions, 63 deletions

diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 58aef9a7b..d0c999196 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -30,23 +30,23 @@ Open Local Scope signature_scope.
 
 (** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
 
-Instance [ ! Equivalence A R ] => 
+Instance [ Equivalence A R ] => 
   equivalence_default : DefaultRelation A R | 4.
 
 Definition equiv [ Equivalence A R ] : relation A := R.
 
 (** Shortcuts to make proof search possible (unification won't unfold equiv). *)
 
-Program Instance [ sa : ! Equivalence A ] => equiv_refl : Reflexive equiv.
+Program Instance [ sa : Equivalence A ] => equiv_refl : Reflexive equiv.
 
-Program Instance [ sa : ! Equivalence A ] => equiv_sym : Symmetric equiv.
+Program Instance [ sa : Equivalence A ] => equiv_sym : Symmetric equiv.
 
   Next Obligation.
   Proof.
     symmetry ; auto.
   Qed.
 
-Program Instance [ sa : ! Equivalence A ] => equiv_trans : Transitive equiv.
+Program Instance [ sa : Equivalence A ] => equiv_trans : Transitive equiv.
 
   Next Obligation.
   Proof.
@@ -81,7 +81,7 @@ Ltac clsubst_nofail :=
 
 Tactic Notation "clsubst" "*" := clsubst_nofail.
 
-Lemma nequiv_equiv_trans : forall [ ! Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z.
+Lemma nequiv_equiv_trans : forall [ Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z.
 Proof with auto.
   intros; intro.
   assert(z === y) by (symmetry ; auto).
@@ -89,7 +89,7 @@ Proof with auto.
   contradiction.
 Qed.
 
-Lemma equiv_nequiv_trans : forall [ ! Equivalence A ] (x y z : A), x === y -> y =/= z -> x =/= z.
+Lemma equiv_nequiv_trans : forall [ Equivalence A ] (x y z : A), x === y -> y =/= z -> x =/= z.
 Proof.
   intros; intro. 
   assert(y === x) by (symmetry ; auto).
@@ -116,12 +116,12 @@ Ltac equivify := repeat equivify_tac.
 
 (** Every equivalence relation gives rise to a morphism, as it is Transitive and Symmetric. *)
 
-Instance [ sa : ! Equivalence ] => equiv_morphism : Morphism (equiv ++> equiv ++> iff) equiv :=
+Instance [ sa : Equivalence ] => equiv_morphism : Morphism (equiv ++> equiv ++> iff) equiv :=
   respect := respect.
 
 (** The partial application too as it is Reflexive. *)
 
-Instance [ sa : ! Equivalence A ] (x : A) => 
+Instance [ sa : Equivalence A ] (x : A) => 
   equiv_partial_app_morphism : Morphism (equiv ++> iff) (equiv x) :=
   respect := respect. 
 
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
index 28fa55ee1..4750df639 100644
--- a/theories/Classes/Functions.v
+++ b/theories/Classes/Functions.v
@@ -21,22 +21,22 @@ Require Import Coq.Classes.Morphisms.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Injective : Prop :=
+Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Injective : Prop :=
   injective : forall x y : A, RB (f x) (f y) -> RA x y.
 
-Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Surjective : Prop :=
+Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Surjective : Prop :=
   surjective : forall y, exists x : A, RB y (f x).
 
-Definition Bijective [ m : ! Morphism (A -> B) (RA ++> RB) (f : A -> B) ] :=
+Definition Bijective [ m : Morphism (A -> B) (RA ++> RB) (f : A -> B) ] :=
   Injective m /\ Surjective m.
 
-Class [ m : ! Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism :=
+Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism :=
   monic :> Injective m.
 
-Class [ m : ! Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism :=
+Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism :=
   epic :> Surjective m.
 
-Class [ m : ! Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism :=
+Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism :=
   monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m.
 
-Class [ m : ! Morphism (A -> A) (eqA ++> eqA), IsoMorphism m ] => AutoMorphism.
+Class [ m : Morphism (A -> A) (eqA ++> eqA), ! IsoMorphism m ] => AutoMorphism.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index f4ec50989..eda2aecaa 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -152,7 +152,7 @@ Proof.
   reduce. apply* H.  apply* sub. assumption.
 Qed.
 
-Lemma subrelation_morphism [ SubRelation A R₁ R₂, Morphism R₂ m ] : Morphism R₁ m.
+Lemma subrelation_morphism [ SubRelation A R₁ R₂, ! Morphism R₂ m ] : Morphism R₁ m.
 Proof.
   intros. apply* H. apply H0.
 Qed.
@@ -177,7 +177,7 @@ Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl
 
 (* Typeclasses eauto := debug. *)
 
-Program Instance [ ! Symmetric A R, Morphism (R ==> impl) m ] => Reflexive_impl_iff : Morphism (R ==> iff) m.
+Program Instance [ Symmetric A R, Morphism _ (R ==> impl) m ] => Reflexive_impl_iff : Morphism (R ==> iff) m.
 
   Next Obligation.
   Proof.
@@ -186,7 +186,7 @@ Program Instance [ ! Symmetric A R, Morphism (R ==> impl) m ] => Reflexive_impl_
 
 (** The complement of a relation conserves its morphisms. *)
 
-Program Instance {A} (RA : relation A) [ mR : Morphism (RA ==> RA ==> iff) R ] => 
+Program Instance [ mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R ] => 
   complement_morphism : Morphism (RA ==> RA ==> iff) (complement R).
 
   Next Obligation.
@@ -200,7 +200,7 @@ Program Instance {A} (RA : relation A) [ mR : Morphism (RA ==> RA ==> iff) R ] =
 
 (** The inverse too. *)
 
-Program Instance {A} (RA : relation A) [ Morphism (RA ==> RA ==> iff) R ] => 
+Program Instance [ Morphism (A -> _) (RA ==> RA ==> iff) R ] => 
   inverse_morphism : Morphism (RA ==> RA ==> iff) (inverse R).
 
   Next Obligation.
@@ -208,7 +208,7 @@ Program Instance {A} (RA : relation A) [ Morphism (RA ==> RA ==> iff) R ] =>
     apply respect ; auto.
   Qed.
 
-Program Instance {A B C : Type} [ Morphism (RA ==> RB ==> RC) (f : A -> B -> C) ] => 
+Program Instance [ Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] => 
   flip_morphism : Morphism (RB ==> RA ==> RC) (flip f).
 
   Next Obligation.
@@ -219,7 +219,7 @@ Program Instance {A B C : Type} [ Morphism (RA ==> RB ==> RC) (f : A -> B -> C)
 (** Every Transitive relation gives rise to a binary morphism on [impl], 
    contravariant in the first argument, covariant in the second. *)
 
-Program Instance [ ! Transitive A (R : relation A) ] => 
+Program Instance [ Transitive A R ] => 
   trans_contra_co_morphism : Morphism (R --> R ++> impl) R.
 
   Next Obligation.
@@ -230,7 +230,7 @@ Program Instance [ ! Transitive A (R : relation A) ] =>
 
 (** Dually... *)
 
-Program Instance [ ! Transitive A (R : relation A) ] =>
+Program Instance [ Transitive A R ] =>
   trans_co_contra_inv_impl_morphism : Morphism (R ++> R --> inverse impl) R.
   
   Next Obligation.
@@ -252,7 +252,7 @@ Program Instance [ ! Transitive A (R : relation A) ] =>
 
 (** Morphism declarations for partial applications. *)
 
-Program Instance [ ! Transitive A R ] (x : A) =>
+Program Instance [ Transitive A R ] (x : A) =>
   trans_contra_inv_impl_morphism : Morphism (R --> inverse impl) (R x).
 
   Next Obligation.
@@ -260,7 +260,7 @@ Program Instance [ ! Transitive A R ] (x : A) =>
     transitivity y...
   Qed.
 
-Program Instance [ ! Transitive A R ] (x : A) =>
+Program Instance [ Transitive A R ] (x : A) =>
   trans_co_impl_morphism : Morphism (R ==> impl) (R x).
 
   Next Obligation.
@@ -268,7 +268,7 @@ Program Instance [ ! Transitive A R ] (x : A) =>
     transitivity x0...
   Qed.
 
-Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
+Program Instance [ Transitive A R, Symmetric A R ] (x : A) =>
   trans_sym_co_inv_impl_morphism : Morphism (R ==> inverse impl) (R x).
 
   Next Obligation.
@@ -276,7 +276,7 @@ Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
     transitivity y...
   Qed.
 
-Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
+Program Instance [ Transitive A R, Symmetric _ R ] (x : A) =>
   trans_sym_contra_impl_morphism : Morphism (R --> impl) (R x).
 
   Next Obligation.
@@ -309,14 +309,13 @@ Program Instance [ Equivalence A R ] (x : A) =>
 
 (** [R] is Reflexive, hence we can build the needed proof. *)
 
-Program Instance (A B : Type) (R : relation A) (R' : relation B)
-  [ Morphism (R ==> R') m ] [ Reflexive R ] (x : A) =>
+Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive _ R ] (x : A) =>
   Reflexive_partial_app_morphism : Morphism R' (m x) | 3.
 
 (** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof
    to get an [R y z] goal. *)
 
-Program Instance [ ! Transitive A R ] => 
+Program Instance [ Transitive A R ] => 
   trans_co_eq_inv_impl_morphism : Morphism (R ==> (@eq A) ==> inverse impl) R.
 
   Next Obligation.
@@ -324,7 +323,7 @@ Program Instance [ ! Transitive A R ] =>
     transitivity y...
   Qed.
 
-Program Instance [ ! Transitive A R ] => 
+Program Instance [ Transitive A R ] => 
   trans_contra_eq_impl_morphism : Morphism (R --> (@eq A) ==> impl) R.
 
   Next Obligation.
@@ -334,7 +333,7 @@ Program Instance [ ! Transitive A R ] =>
 
 (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
 
-Program Instance [ ! Transitive A R, Symmetric R ] => 
+Program Instance [ Transitive A R, Symmetric _ R ] => 
   trans_sym_morphism : Morphism (R ==> R ==> iff) R.
 
   Next Obligation.
@@ -421,11 +420,11 @@ Program Instance or_iff_morphism :
 (*   red ; intros. subst ; split; trivial. *)
 (* Qed. *)
 
-Instance (A B : Type) [ ! Reflexive B R ] (m : A -> B) =>
-  eq_Reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3.
+Instance (A : Type) [ Reflexive B R ] (m : A -> B) =>
+  eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3.
 Proof. simpl_relation. Qed.
 
-Instance (A B : Type) [ ! Reflexive B R' ] => 
+Instance (A : Type) [ Reflexive B R' ] => 
   Reflexive (@Logic.eq A ==> R').
 Proof. simpl_relation. Qed.
 
@@ -469,9 +468,8 @@ Proof.
   symmetry ; apply inverse_respectful.
 Qed.
 
-Instance (A : Type) (R : relation A) (B : Type) (R' R'' : relation B) 
-  [ Normalizes relation_equivalence R' (inverse R'') ] =>
-  Normalizes relation_equivalence (inverse R ==> R') (inverse (R ==> R'')) .
+Instance [ Normalizes (relation B) relation_equivalence R' (inverse R'') ] =>
+  ! Normalizes (relation (A -> B)) relation_equivalence (inverse R ==> R') (inverse (R ==> R'')) .
 Proof.
   red.
   pose normalizes.
@@ -480,9 +478,8 @@ Proof.
   reflexivity.
 Qed.
 
-Program Instance (A : Type) (R : relation A)
-  [ Morphism R m ] => morphism_inverse_morphism :
-  Morphism (inverse R) m | 2.
+Program Instance [ Morphism A R m ] => 
+  morphism_inverse_morphism : Morphism (inverse R) m | 2.
 
 (** Bootstrap !!! *)
 
@@ -497,9 +494,9 @@ Proof.
   apply respect.
 Qed.
   
-Lemma morphism_releq_morphism (A : Type) (R : relation A) (R' : relation A)
-  [ Normalizes relation_equivalence R R' ]
-  [ Morphism R' m ] : Morphism R m.
+Lemma morphism_releq_morphism 
+  [ Normalizes (relation A) relation_equivalence R R',
+    Morphism _ R' m ] : Morphism R m.
 Proof.
   intros.
   pose respect.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 492b8498a..0ca074589 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -75,48 +75,48 @@ Hint Resolve @irreflexivity : ord.
 
 (** We can already dualize all these properties. *)
 
-Program Instance [ ! Reflexive A R ] => flip_Reflexive : Reflexive (flip R) :=
+Program Instance [ Reflexive A R ] => flip_Reflexive : Reflexive (flip R) :=
   reflexivity := reflexivity (R:=R).
 
-Program Instance [ ! Irreflexive A R ] => flip_Irreflexive : Irreflexive (flip R) :=
+Program Instance [ Irreflexive A R ] => flip_Irreflexive : Irreflexive (flip R) :=
   irreflexivity := irreflexivity (R:=R).
 
-Program Instance [ ! Symmetric A R ] => flip_Symmetric : Symmetric (flip R).
+Program Instance [ Symmetric A R ] => flip_Symmetric : Symmetric (flip R).
 
   Solve Obligations using unfold flip ; program_simpl ; clapply Symmetric.
 
-Program Instance [ ! Asymmetric A R ] => flip_Asymmetric : Asymmetric (flip R).
+Program Instance [ Asymmetric A R ] => flip_Asymmetric : Asymmetric (flip R).
   
   Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetry.
 
-Program Instance [ ! Transitive A R ] => flip_Transitive : Transitive (flip R).
+Program Instance [ Transitive A R ] => flip_Transitive : Transitive (flip R).
 
   Solve Obligations using unfold flip ; program_simpl ; clapply transitivity.
 
 (** Have to do it again for Prop. *)
 
-Program Instance [ ! Reflexive A (R : relation A) ] => inverse_Reflexive : Reflexive (inverse R) :=
+Program Instance [ Reflexive A (R : relation A) ] => inverse_Reflexive : Reflexive (inverse R) :=
   reflexivity := reflexivity (R:=R).
 
-Program Instance [ ! Irreflexive A (R : relation A) ] => inverse_Irreflexive : Irreflexive (inverse R) :=
+Program Instance [ Irreflexive A (R : relation A) ] => inverse_Irreflexive : Irreflexive (inverse R) :=
   irreflexivity := irreflexivity (R:=R).
 
-Program Instance [ ! Symmetric A (R : relation A) ] => inverse_Symmetric : Symmetric (inverse R).
+Program Instance [ Symmetric A (R : relation A) ] => inverse_Symmetric : Symmetric (inverse R).
 
   Solve Obligations using unfold inverse, flip ; program_simpl ; clapply Symmetric.
 
-Program Instance [ ! Asymmetric A (R : relation A) ] => inverse_Asymmetric : Asymmetric (inverse R).
+Program Instance [ Asymmetric A (R : relation A) ] => inverse_Asymmetric : Asymmetric (inverse R).
   
   Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; clapply asymmetry.
 
-Program Instance [ ! Transitive A (R : relation A) ] => inverse_Transitive : Transitive (inverse R).
+Program Instance [ Transitive A (R : relation A) ] => inverse_Transitive : Transitive (inverse R).
 
   Solve Obligations using unfold inverse, flip ; program_simpl ; clapply transitivity.
 
-Program Instance [ ! Reflexive A (R : relation A) ] => 
+Program Instance [ Reflexive A (R : relation A) ] => 
   Reflexive_complement_Irreflexive : Irreflexive (complement R).
 
-Program Instance [ ! Irreflexive A (R : relation A) ] => 
+Program Instance [ Irreflexive A (R : relation A) ] => 
   Irreflexive_complement_Reflexive : Reflexive (complement R).
 
   Next Obligation. 
@@ -125,7 +125,7 @@ Program Instance [ ! Irreflexive A (R : relation A) ] =>
     apply (irreflexivity H).
   Qed.
 
-Program Instance [ ! Symmetric A (R : relation A) ] => complement_Symmetric : Symmetric (complement R).
+Program Instance [ Symmetric A (R : relation A) ] => complement_Symmetric : Symmetric (complement R).
 
   Next Obligation.
   Proof.
@@ -210,10 +210,10 @@ Class Equivalence (carrier : Type) (equiv : relation carrier) :=
 Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := 
   antisymmetry : forall x y, R x y -> R y x -> eqA x y.
 
-Program Instance [ eq : Equivalence A eqA, Antisymmetric eq R ] => 
+Program Instance [ eq : Equivalence A eqA, ! Antisymmetric eq R ] => 
   flip_antiSymmetric : Antisymmetric eq (flip R).
 
-Program Instance [ eq : Equivalence A eqA, Antisymmetric eq (R : relation A) ] => 
+Program Instance [ eq : Equivalence A eqA, ! Antisymmetric eq (R : relation A) ] => 
   inverse_antiSymmetric : Antisymmetric eq (inverse R).
 
 (** Leibinz equality [eq] is an equivalence relation. *)
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 86a2bef80..26e1ab244 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -54,7 +54,7 @@ Open Local Scope program_scope.
 
 (** Invert the branches. *)
 
-Program Definition nequiv_dec [ ! EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
+Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
 
 (** Overloaded notation for inequality. *)
 
@@ -62,10 +62,10 @@ Infix "=/=" := nequiv_dec (no associativity, at level 70).
 
 (** Define boolean versions, losing the logical information. *)
 
-Definition equiv_decb [ ! EqDec A ] (x y : A) : bool :=
+Definition equiv_decb [ EqDec A ] (x y : A) : bool :=
   if x == y then true else false.
 
-Definition nequiv_decb [ ! EqDec A ] (x y : A) : bool :=
+Definition nequiv_decb [ EqDec A ] (x y : A) : bool :=
   negb (equiv_decb x y).
 
 Infix "==b" := equiv_decb (no associativity, at level 70).
@@ -97,7 +97,7 @@ Program Instance unit_eqdec : EqDec (@eq_setoid unit) :=
     reflexivity.
   Qed.
 
-Program Instance [ EqDec (@eq_setoid A), EqDec (@eq_setoid B) ] => 
+Program Instance [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] => 
   prod_eqdec : EqDec (@eq_setoid (prod A B)) :=
   equiv_dec x y := 
     dest x as (x1, x2) in 
@@ -113,7 +113,7 @@ Program Instance [ EqDec (@eq_setoid A), EqDec (@eq_setoid B) ] =>
 
 Require Import Coq.Program.FunctionalExtensionality.
 
-Program Instance [ EqDec (@eq_setoid A) ] => bool_function_eqdec : EqDec (@eq_setoid (bool -> A)) :=
+Program Instance [ ! EqDec (@eq_setoid A) ] => bool_function_eqdec : EqDec (@eq_setoid (bool -> A)) :=
   equiv_dec f g := 
     if f true == g true then
       if f false == g false then in_left