Generalized binding syntax overhaul: only two new binders: `() and `{},

guessing the binding name by default and making all generalized
variables implicit. At the same time, continue refactoring of
Record/Class/Inductive etc.., getting rid of [VernacRecord]
definitively. The AST is not completely satisfying, but leaning towards 
Record/Class as restrictions of inductive (Arnaud, anyone ?).
Now, [Class] declaration bodies are either of the form [meth : type] or 
[{ meth : type ; ... }], distinguishing singleton "definitional" classes
and inductive classes based on records. The constructor syntax is
accepted ([meth1 : type1 | meth1 : type2]) but raises an error
immediately, as support for defining a class by a general inductive type
is not there yet (this is a bugfix!).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11679 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 469147cf4..3fcbac061 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -27,7 +27,7 @@ Unset Strict Implicit.
 
 Open Local Scope signature_scope.
 
-Definition equiv [ Equivalence A R ] : relation A := R.
+Definition equiv `{Equivalence A R} : relation A := R.
 
 (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
 
@@ -39,7 +39,7 @@ Open Local Scope equiv_scope.
 
 (** Overloading for [PER]. *)
 
-Definition pequiv [ PER A R ] : relation A := R.
+Definition pequiv `{PER A R} : relation A := R.
 
 (** Overloaded notation for partial equivalence. *)
 
@@ -47,11 +47,11 @@ Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope.
 
 (** Shortcuts to make proof search easier. *)
 
-Program Instance equiv_reflexive [ sa : Equivalence A ] : Reflexive equiv.
+Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv.
 
-Program Instance equiv_symmetric [ sa : Equivalence A ] : Symmetric equiv.
+Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv.
 
-Program Instance equiv_transitive [ sa : Equivalence A ] : Transitive equiv.
+Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv.
 
   Next Obligation.
   Proof.
@@ -103,10 +103,10 @@ Section Respecting.
   (** Here we build an equivalence instance for functions which relates respectful ones only, 
      we do not export it. *)
 
-  Definition respecting {( eqa : Equivalence A (R : relation A), eqb : Equivalence B (R' : relation B) )} : Type := 
+  Definition respecting `(eqa : Equivalence A (R : relation A), eqb : Equivalence B (R' : relation B)) : Type := 
     { morph : A -> B | respectful R R' morph morph }.
   
-  Program Instance respecting_equiv [ eqa : Equivalence A R, eqb : Equivalence B R' ] :
+  Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') :
     Equivalence (fun (f g : respecting eqa eqb) => 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.
@@ -120,7 +120,7 @@ End Respecting.
 
 (** The default equivalence on function spaces, with higher-priority than [eq]. *)
 
-Program Instance pointwise_equivalence A ((eqb : Equivalence B eqB)) :
+Program Instance pointwise_equivalence {A} `(eqb : Equivalence B eqB) :
   Equivalence (pointwise_relation A eqB) | 9.
 
   Next Obligation.