Open notation for declaring record instances.

It solves feature request 1852, makes me and Arnaud happy and 
will permit to factor some more code in typeclasses.
- Records are introduced using the syntax "{| x := t; y := foo |}" and
"with" clauses are currently parsed but not yet supported in the
elaboration. You are invited to suggest other syntaxes :)
- Missing fields are turned into holes, extra fields cause an error
message. The current implementation finds the type of the record
at pretyping time, from the typing constraint alone (and just expects
an inductive with one constructor). It is then impossible to use
scope information to parse the bodies: that may be wrong. The other
solution I see is using the fields to detect the type earlier, before
internalisation of the bodies, but then we get in name clash hell.
- In funind/contrib/interface I mostly put [assert false] everywhere to 
avoid warnings.


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

1 files changed, 1 insertions, 1 deletions

diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 97fbae075..c437d9eab 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -25,7 +25,7 @@ open Util
 (* This module defines type-classes *)
 type typeclass = {
   (* The class implementation: a record parameterized by the context with defs in it or a definition if 
-     the class is a singleton. This acts as the classe's global identifier. *)
+     the class is a singleton. This acts as the class' global identifier. *)
   cl_impl : global_reference; 
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses.