summaryrefslogtreecommitdiff
path: root/pretyping/typeclasses.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /pretyping/typeclasses.mli
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'pretyping/typeclasses.mli')
-rw-r--r--pretyping/typeclasses.mli22
1 files changed, 14 insertions, 8 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index fdbb78a9..d8e15895 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: typeclasses.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: typeclasses.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
(*i*)
open Names
@@ -25,18 +25,20 @@ 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.
- The boolean indicates if the typeclass argument is a direct superclass. *)
- cl_context : ((global_reference * bool) option * rel_declaration) list;
+ The boolean indicates if the typeclass argument is a direct superclass and the global reference
+ gives a direct link to the class itself. *)
+ cl_context : (global_reference * bool) option list * rel_context;
(* Context of definitions and properties on defs, will not be shared *)
cl_props : rel_context;
- (* The methods implementations of the typeclass as projections. *)
- cl_projs : (identifier * constant) list;
+ (* The methods implementations of the typeclass as projections. Some may be undefinable due to
+ sorting restrictions. *)
+ cl_projs : (identifier * constant option) list;
}
type instance
@@ -52,9 +54,13 @@ val add_instance : instance -> unit
val class_info : global_reference -> typeclass (* raises a UserError if not a class *)
-val class_of_constr : constr -> typeclass option
-val dest_class_app : constr -> typeclass * constr array (* raises a UserError if not a class *)
+(* These raise a UserError if not a class. *)
+val dest_class_app : env -> constr -> typeclass * constr list
+
+(* Just return None if not a class *)
+val class_of_constr : constr -> typeclass option
+
val instance_impl : instance -> constant
val is_class : global_reference -> bool