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, 5 insertions, 5 deletions

diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 6a5eafe8b..1e19f66b8 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -276,14 +276,14 @@ Ltac simpl_depind_r := subst_right_no_fail ; autoinjections_right ; try discrimi
    [injection] tactics on which we can always fall back.
    *)
   
-Class NoConfusionPackage (I : Type) := NoConfusion : Π P : Prop, Type ; noConfusion : Π P, NoConfusion P.
+Class NoConfusionPackage (I : Type) := { NoConfusion : Π P : Prop, Type ; noConfusion : Π P, NoConfusion P }.
 
 (** The [DependentEliminationPackage] provides the default dependent elimination principle to
    be used by the [equations] resolver. It is especially useful to register the dependent elimination
    principles for things in [Prop] which are not automatically generated. *)
 
 Class DependentEliminationPackage (A : Type) :=
-  elim_type : Type ; elim : elim_type.
+  { elim_type : Type ; elim : elim_type }.
 
 (** A higher-order tactic to apply a registered eliminator. *)
 
@@ -302,14 +302,14 @@ Ltac elim_ind p := elim_tac ltac:(fun p el => induction p using el) p.
 (** The [BelowPackage] class provides the definition of a [Below] predicate for some datatype,
    allowing to talk about course-of-value recursion on it. *)
 
-Class BelowPackage (A : Type) :=
+Class BelowPackage (A : Type) := {
   Below : A -> Type ;
-  below : Π (a : A), Below a.
+  below : Π (a : A), Below a }.
 
 (** The [Recursor] class defines a recursor on a type, based on some definition of [Below]. *)
 
 Class Recursor (A : Type) (BP : BelowPackage A) := 
-  rec_type : A -> Type ; rec : Π (a : A), rec_type a.
+  { rec_type : A -> Type ; rec : Π (a : A), rec_type a }.
 
 (** Lemmas used by the simplifier, mainly rephrasings of [eq_rect], [eq_ind]. *)