- Cleanup parsing of binders, reducing to a single production for all

  binders.
- Change syntax of type class instances to better match the usual syntax of
  lemmas/definitions with name first, then arguments ":" instance.
  Update theories/Classes accordingly.
- Correct globalization of tactic references when doing Ltac :=/::=, update
  documentation.
- Remove the not so useful "(x &)" and "{{x}}" syntaxes from
  Program.Utils, and subset_scope as well.


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

7 files changed, 73 insertions, 76 deletions

diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 62744b1d1..d96a532c3 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -94,8 +94,8 @@ Program Instance unit_eqdec : ! EqDec unit eq :=
     reflexivity.
   Qed.
 
-Program Instance [ EqDec A eq, EqDec B eq ] => 
-  prod_eqdec : ! EqDec (prod A B) eq :=
+Program Instance prod_eqdec [ EqDec A eq, EqDec B eq ] :
+  ! EqDec (prod A B) eq :=
   equiv_dec x y := 
     let '(x1, x2) := x in 
     let '(y1, y2) := y in 
@@ -106,8 +106,8 @@ Program Instance [ EqDec A eq, EqDec B eq ] =>
 
   Solve Obligations using unfold complement, equiv ; program_simpl.
 
-Program Instance [ EqDec A eq, EqDec B eq ] => 
-  sum_eqdec : ! EqDec (sum A B) eq :=
+Program Instance sum_eqdec [ EqDec A eq, EqDec B eq ] :
+  ! EqDec (sum A B) eq :=
   equiv_dec x y := 
     match x, y with
       | inl a, inl b => if a == b then in_left else in_right
@@ -121,7 +121,7 @@ Program Instance [ EqDec A eq, EqDec B eq ] =>
 
 Require Import Coq.Program.FunctionalExtensionality.
 
-Program Instance [ EqDec A eq ] => bool_function_eqdec : ! EqDec (bool -> A) eq :=
+Program Instance bool_function_eqdec [ EqDec A eq ] : ! EqDec (bool -> A) eq :=
   equiv_dec f g := 
     if f true == g true then
       if f false == g false then in_left
@@ -138,7 +138,7 @@ Program Instance [ EqDec A eq ] => bool_function_eqdec : ! EqDec (bool -> A) eq
 
 Require Import List.
 
-Program Instance [ eqa : EqDec A eq ] => list_eqdec : ! EqDec (list A) eq :=
+Program Instance list_eqdec [ eqa : EqDec A eq ] : ! EqDec (list A) eq :=
   equiv_dec := 
     fix aux (x : list A) y { struct x } :=
     match x, y with
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 23af8a744..42961baea 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -52,16 +52,16 @@ Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope.
 
 (** Shortcuts to make proof search easier. *)
 
-Program Instance [ sa : Equivalence A ] => equiv_reflexive : Reflexive equiv.
+Program Instance equiv_reflexive [ sa : Equivalence A ] : Reflexive equiv.
 
-Program Instance [ sa : Equivalence A ] => equiv_symmetric : Symmetric equiv.
+Program Instance equiv_symmetric [ sa : Equivalence A ] : Symmetric equiv.
 
   Next Obligation.
   Proof.
     symmetry ; auto.
   Qed.
 
-Program Instance [ sa : Equivalence A ] => equiv_transitive : Transitive equiv.
+Program Instance equiv_transitive [ sa : Equivalence A ] : Transitive equiv.
 
   Next Obligation.
   Proof.
@@ -116,8 +116,8 @@ Section Respecting.
   Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := 
     { morph : A -> B | respectful R R' morph morph }.
   
-  Program Instance [ Equivalence A R, Equivalence B R' ] => 
-    respecting_equiv : Equivalence respecting
+  Program Instance respecting_equiv [ Equivalence A R, Equivalence B R' ] :
+    Equivalence respecting
     (fun (f g : respecting) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
 
   Solve Obligations using unfold respecting in * ; simpl_relation ; program_simpl.
@@ -134,8 +134,8 @@ End Respecting.
 
 (** The default equivalence on function spaces, with higher-priority than [eq]. *)
 
-Program Instance [ Equivalence A eqA ] => 
-  pointwise_equivalence : Equivalence (B -> A) (pointwise_relation eqA) | 9.
+Program Instance pointwise_equivalence [ Equivalence A eqA ] :
+  Equivalence (B -> A) (pointwise_relation eqA) | 9.
 
   Next Obligation.
   Proof.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 5ac6d8ee5..cd38f318c 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -87,12 +87,12 @@ Proof. firstorder. Qed.
 
 (** The subrelation property goes through products as usual. *)
 
-Instance [ sub : subrelation A R₁ R₂ ] =>
-  morphisms_subrelation : ! subrelation (B -> A) (R ==> R₁) (R ==> R₂).
+Instance morphisms_subrelation [ sub : subrelation A R₁ R₂ ] :
+  ! subrelation (B -> A) (R ==> R₁) (R ==> R₂).
 Proof. firstorder. Qed.
 
-Instance [ sub : subrelation A R₂ R₁ ] =>
-  morphisms_subrelation_left : ! subrelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3.
+Instance morphisms_subrelation_left [ sub : subrelation A R₂ R₁ ] :
+  ! subrelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3.
 Proof. firstorder. Qed.
 
 (** [Morphism] is itself a covariant morphism for [subrelation]. *)
@@ -129,16 +129,15 @@ Proof. firstorder. Qed.
 Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl).
 Proof. firstorder. Qed.
 
-Instance [ sub : subrelation A R R' ] => pointwise_subrelation :
+Instance pointwise_subrelation [ sub : subrelation A R R' ] :
   subrelation (pointwise_relation (A:=B) R) (pointwise_relation R') | 4.
 Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed.
 
 (** The complement of a relation conserves its morphisms. *)
 
-Program Instance [ mR : Morphism (A -> A -> Prop)
-  (RA ==> RA ==> iff) R ] => 
-  complement_morphism : Morphism (RA ==> RA ==> iff)
-  (complement R).
+Program Instance complement_morphism
+  [ mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R ] :
+  Morphism (RA ==> RA ==> iff) (complement R).
 
   Next Obligation.
   Proof.
@@ -149,8 +148,9 @@ Program Instance [ mR : Morphism (A -> A -> Prop)
 
 (** The [inverse] too, actually the [flip] instance is a bit more general. *) 
 
-Program Instance [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] => 
-  flip_morphism : Morphism (RB ==> RA ==> RC) (flip f).
+Program Instance flip_morphism
+  [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] :
+  Morphism (RB ==> RA ==> RC) (flip f).
 
   Next Obligation.
   Proof.
@@ -160,8 +160,8 @@ Program Instance [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] =>
 (** 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 ] => 
-  trans_contra_co_morphism : Morphism (R --> R ++> impl) R.
+Program Instance trans_contra_co_morphism
+  [ Transitive A R ] : Morphism (R --> R ++> impl) R.
 
   Next Obligation.
   Proof with auto.
@@ -181,40 +181,40 @@ Program Instance [ Transitive A R ] =>
 
 (** Morphism declarations for partial applications. *)
 
-Program Instance [ Transitive A R ] =>
-  trans_contra_inv_impl_morphism : Morphism (R --> inverse impl) (R x).
+Program Instance trans_contra_inv_impl_morphism
+  [ Transitive A R ] : Morphism (R --> inverse impl) (R x).
 
   Next Obligation.
   Proof with auto.
     transitivity y...
   Qed.
 
-Program Instance [ Transitive A R ] =>
-  trans_co_impl_morphism : Morphism (R ==> impl) (R x).
+Program Instance trans_co_impl_morphism
+  [ Transitive A R ] : Morphism (R ==> impl) (R x).
 
   Next Obligation.
   Proof with auto.
     transitivity x0...
   Qed.
 
-Program Instance [ Transitive A R, Symmetric A R ] =>
-  trans_sym_co_inv_impl_morphism : Morphism (R ==> inverse impl) (R x).
+Program Instance trans_sym_co_inv_impl_morphism
+  [ Transitive A R, Symmetric A R ] : Morphism (R ==> inverse impl) (R x).
 
   Next Obligation.
   Proof with auto.
     transitivity y...
   Qed.
 
-Program Instance [ Transitive A R, Symmetric _ R ] =>
-  trans_sym_contra_impl_morphism : Morphism (R --> impl) (R x).
+Program Instance trans_sym_contra_impl_morphism
+  [ Transitive A R, Symmetric _ R ] : Morphism (R --> impl) (R x).
 
   Next Obligation.
   Proof with auto.
     transitivity x0...
   Qed.
 
-Program Instance [ Equivalence A R ] =>
-  equivalence_partial_app_morphism : Morphism (R ==> iff) (R x).
+Program Instance equivalence_partial_app_morphism
+  [ Equivalence A R ] : Morphism (R ==> iff) (R x).
 
   Next Obligation.
   Proof with auto.
@@ -227,8 +227,8 @@ Program Instance [ Equivalence A R ] =>
 (** 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 ] => 
-  trans_co_eq_inv_impl_morphism : Morphism (R ==> (@eq A) ==> inverse impl) R.
+Program Instance trans_co_eq_inv_impl_morphism
+  [ Transitive A R ] : Morphism (R ==> (@eq A) ==> inverse impl) R.
 
   Next Obligation.
   Proof with auto.
@@ -245,8 +245,8 @@ Program Instance [ Transitive A R ] =>
 
 (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
 
-Program Instance [ Transitive A R, Symmetric _ R ] => 
-  trans_sym_morphism : Morphism (R ==> R ==> iff) R.
+Program Instance trans_sym_morphism
+  [ Transitive A R, Symmetric _ R ] : Morphism (R ==> R ==> iff) R.
 
   Next Obligation.
   Proof with auto.
@@ -256,8 +256,8 @@ Program Instance [ Transitive A R, Symmetric _ R ] =>
     transitivity y... transitivity y0... 
   Qed.
 
-Program Instance [ Equivalence A R ] =>
-  equiv_morphism : Morphism (R ==> R ==> iff) R.
+Program Instance equiv_morphism [ Equivalence A R ] :
+  Morphism (R ==> R ==> iff) R.
 
   Next Obligation.
   Proof with auto.
@@ -288,7 +288,7 @@ Program Instance inverse_iff_impl_id :
 (*   eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *)
 (* Proof. simpl_relation. Qed. *)
 
-Instance (A : Type) [ Reflexive B R' ] =>
+Instance reflexive_eq_dom_reflexive (A : Type) [ Reflexive B R' ] :
   Reflexive (@Logic.eq A ==> R').
 Proof. simpl_relation. Qed.
 
@@ -322,12 +322,12 @@ Qed.
 Class MorphismProxy A (R : relation A) (m : A) : Prop :=
   respect_proxy : R m m.
 
-Instance [ Reflexive A R ] (x : A) => 
-  reflexive_morphism_proxy : MorphismProxy A R x | 1.
+Instance reflexive_morphism_proxy
+  [ Reflexive A R ] (x : A) : MorphismProxy A R x | 1.
 Proof. firstorder. Qed.
 
-Instance [ Morphism A R x ] =>
-  morphism_morphism_proxy : MorphismProxy A R x | 2.
+Instance morphism_morphism_proxy
+  [ Morphism A R x ] : MorphismProxy A R x | 2.
 Proof. firstorder. Qed.
 
 (* Instance (A : Type) [ Reflexive B R ] => *)
@@ -392,8 +392,8 @@ 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'') ] =>
-  inverse_respectful_rec_norm : Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')).
+Instance inverse_respectful_rec_norm [ Normalizes B R' (inverse R'') ] :
+  Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')).
 Proof. red ; intros.  
   pose normalizes as r.
   setoid_rewrite r.
@@ -403,8 +403,8 @@ Qed.
 
 (** Once we have normalized, we will apply this instance to simplify the problem. *)
 
-Program Instance [ Morphism A R m ] => 
-  morphism_inverse_morphism : Morphism (inverse R) m | 2.
+Program Instance morphism_inverse_morphism
+  [ Morphism A R m ] : Morphism (inverse R) m | 2.
 
 (** Bootstrap !!! *)
 
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index 301fba534..7dc1f95ef 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -73,7 +73,7 @@ Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl
 
 (** Morphisms for quantifiers *)
 
-Program Instance {A : Type} => ex_iff_morphism : Morphism (pointwise_relation iff ==> iff) (@ex A).
+Program Instance ex_iff_morphism {A : Type} : Morphism (pointwise_relation iff ==> iff) (@ex A).
 
   Next Obligation.
   Proof.
@@ -86,7 +86,7 @@ Program Instance {A : Type} => ex_iff_morphism : Morphism (pointwise_relation if
     exists x₁. rewrite H. assumption.
   Qed.
 
-Program Instance {A : Type} => ex_impl_morphism :
+Program Instance ex_impl_morphism {A : Type} :
   Morphism (pointwise_relation impl ==> impl) (@ex A).
 
   Next Obligation.
@@ -95,7 +95,7 @@ Program Instance {A : Type} => ex_impl_morphism :
     exists H0. apply H. assumption.
   Qed.
 
-Program Instance {A : Type} => ex_inverse_impl_morphism : 
+Program Instance ex_inverse_impl_morphism {A : Type} : 
   Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@ex A).
 
   Next Obligation.
@@ -104,7 +104,7 @@ Program Instance {A : Type} => ex_inverse_impl_morphism :
     exists H0. apply H. assumption.
   Qed.
 
-Program Instance {A : Type} => all_iff_morphism : 
+Program Instance all_iff_morphism {A : Type} : 
   Morphism (pointwise_relation iff ==> iff) (@all A).
 
   Next Obligation.
@@ -113,7 +113,7 @@ Program Instance {A : Type} => all_iff_morphism :
     intuition ; specialize (H x0) ; intuition.
   Qed.
 
-Program Instance {A : Type} => all_impl_morphism : 
+Program Instance all_impl_morphism {A : Type} : 
   Morphism (pointwise_relation impl ==> impl) (@all A).
   
   Next Obligation.
@@ -122,7 +122,7 @@ Program Instance {A : Type} => all_impl_morphism :
     intuition ; specialize (H x0) ; intuition.
   Qed.
 
-Program Instance {A : Type} => all_inverse_impl_morphism : 
+Program Instance all_inverse_impl_morphism {A : Type} : 
   Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@all A).
   
   Next Obligation.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 015eb7323..25316c278 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -65,26 +65,26 @@ Unset Implicit Arguments.
 
 (** We can already dualize all these properties. *)
 
-Program Instance [ Reflexive A R ] => flip_Reflexive : Reflexive (flip R) :=
+Program Instance flip_Reflexive [ Reflexive A R ] : Reflexive (flip R) :=
   reflexivity := reflexivity (R:=R).
 
-Program Instance [ Irreflexive A R ] => flip_Irreflexive : Irreflexive (flip R) :=
+Program Instance flip_Irreflexive [ Irreflexive A R ] : Irreflexive (flip R) :=
   irreflexivity := irreflexivity (R:=R).
 
-Program Instance [ Symmetric A R ] => flip_Symmetric : Symmetric (flip R).
+Program Instance flip_Symmetric [ Symmetric A R ] : Symmetric (flip R).
 
   Solve Obligations using unfold flip ; program_simpl ; clapply Symmetric.
 
-Program Instance [ Asymmetric A R ] => flip_Asymmetric : Asymmetric (flip R).
+Program Instance flip_Asymmetric [ Asymmetric A R ] : 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 flip_Transitive [ Transitive A R ] : Transitive (flip R).
 
   Solve Obligations using unfold flip ; program_simpl ; clapply transitivity.
 
-Program Instance [ Reflexive A (R : relation A) ] => 
-  Reflexive_complement_Irreflexive : Irreflexive (complement R).
+Program Instance Reflexive_complement_Irreflexive [ Reflexive A (R : relation A) ]
+   : Irreflexive (complement R).
 
   Next Obligation. 
   Proof. 
@@ -95,7 +95,7 @@ Program Instance [ Reflexive A (R : relation A) ] =>
   Qed.
 
 
-Program Instance [ Symmetric A (R : relation A) ] => complement_Symmetric : Symmetric (complement R).
+Program Instance complement_Symmetric [ Symmetric A (R : relation A) ] : Symmetric (complement R).
 
   Next Obligation.
   Proof.
@@ -165,8 +165,7 @@ Class PER (carrier : Type) (pequiv : relation carrier) : Prop :=
 (** We can build a PER on the Coq function space if we have PERs on the domain and
    codomain. *)
 
-Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] => 
-  arrow_per : PER (A -> B)
+Program Instance arrow_per [ PER A (R : relation A), PER B (R' : relation B) ] : PER (A -> B)
   (fun f g => forall (x y : A), R x y -> R' (f x) (g y)).
 
   Next Obligation.
@@ -188,8 +187,8 @@ Class Equivalence (carrier : Type) (equiv : relation carrier) : Prop :=
 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 ] => 
-  flip_antiSymmetric : Antisymmetric eq (flip R).
+Program Instance flip_antiSymmetric [ eq : Equivalence A eqA, ! Antisymmetric eq R ] :
+  Antisymmetric eq (flip R).
 
 (** Leibinz equality [eq] is an equivalence relation.
    The instance has low priority as it is always applicable 
@@ -368,7 +367,7 @@ Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relatio
 
 (** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
 
-Instance (A : Type) => relation_equivalence_equivalence :
+Instance relation_equivalence_equivalence (A : Type) :
   Equivalence (relation A) relation_equivalence.
 Proof. intro A. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed.
 
@@ -387,7 +386,7 @@ Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder :=
    for equivalence (see Morphisms).
    It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *)
 
-Instance [ PartialOrder A eqA R ] =>  partial_order_antisym : ! Antisymmetric A eqA R.
+Instance partial_order_antisym [ PartialOrder A eqA R ] : ! Antisymmetric A eqA R.
 Proof with auto.
   reduce_goal. pose partial_order_equivalence as poe. do 3 red in poe. 
   apply <- poe. firstorder.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 639b15f50..4d6601a6e 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -95,8 +95,7 @@ Program Instance unit_eqdec : EqDec (@eq_setoid unit) :=
     reflexivity.
   Qed.
 
-Program Instance [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] => 
-  prod_eqdec : EqDec (@eq_setoid (prod A B)) :=
+Program Instance prod_eqdec [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] : EqDec (@eq_setoid (prod A B)) :=
   equiv_dec x y := 
     let '(x1, x2) := x in 
     let '(y1, y2) := y in 
@@ -111,7 +110,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 bool_function_eqdec [ ! EqDec (@eq_setoid A) ] : EqDec (@eq_setoid (bool -> A)) :=
   equiv_dec f g := 
     if f true == g true then
       if f false == g false then in_left
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 8412cc102..aeaa197e8 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -38,8 +38,7 @@ Definition default_relation [ DefaultRelation A R ] := R.
 
 (** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
 
-Instance [ Equivalence A R ] => 
-  equivalence_default : DefaultRelation A R | 4.
+Instance equivalence_default [ Equivalence A R ] : DefaultRelation A R | 4.
 
 (** The setoid_replace tactics in Ltac, defined in terms of default relations and
    the setoid_rewrite tactic. *)