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

1 files changed, 8 insertions, 8 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.