Cleaner quantifiers for type classes, breaks clrewrite for the moment but implementation is much less add-hoc. Opens possibility of arbitrary prefixes in Class and Instance declarations. Current implementation with eauto is a bit more dangerous... next patch will fix it.

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

1 files changed, 13 insertions, 10 deletions

diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index f53ea7beac..47cb93a149 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -23,22 +23,25 @@ open Util
 
 (* This module defines type-classes *)
 type typeclass = {
-  cl_name : identifier; (* Name of the class *)
-  cl_context : named_context; (* Context in which superclasses and params are typed (usually types and indirect superclasses) *)
-  cl_super : named_context; (* Direct superclasses applied to some of the params *)
-  cl_params : named_context; (* Context of the real parameters (types and operations) *)
-(*   cl_defs : rel_context; (\* Context of the definitions (usually functions), which may be shared *\) *)
-  cl_props : named_context; (* Context of the properties on defs, in Prop, will not be shared *)
-  cl_impl : inductive; (* The class implementation: a record parameterized by params and defs *)
+  (* Name of the class. FIXME: should not necessarily be globally unique. *)
+  cl_name : identifier;
+
+  (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
+  cl_context : (identifier option * named_declaration) list; 
+
+  cl_params : int; (* This is the length of the suffix of the context which should be considered explicit parameters. *)
+
+  (* Context of definitions and properties on defs, will not be shared *)
+  cl_props : named_context;
+
+  (* The class implementation: a record parameterized by the context with defs in it. *)
+  cl_impl : inductive; 
 }
 
 type instance = {
   is_class: typeclass;
   is_name: identifier; (* Name of the instance *)
-(*   is_params: named_context; (\* Context of the parameters, instanciated *\) *)
-(*   is_super: named_context; (\* The corresponding superclasses *\) *)
   is_impl: constant; 
-(*   is_add_hint : unit -> unit; (\* Hook to add an hint for the instance *\) *)
 }
   
 val instances : Libnames.reference -> instance list