From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 pretyping/typeclasses.mli | 39 ++++++++++++++++++++++-----------------
 1 file changed, 22 insertions(+), 17 deletions(-)

(limited to 'pretyping/typeclasses.mli')

diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index d8e15895..997b28c1 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 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
@@ -24,19 +24,19 @@ 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 implementation: a record parameterized by the context with defs in it or a definition if
      the class is a singleton. This acts as the class' global identifier. *)
-  cl_impl : global_reference; 
+  cl_impl : global_reference;
 
-  (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. 
+  (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
      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; 
+  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. Some may be undefinable due to 
+  (* The methods implementations of the typeclass as projections. Some may be undefinable due to
      sorting restrictions. *)
   cl_projs : (identifier * constant option) list;
 }
@@ -49,7 +49,11 @@ val all_instances : unit -> instance list
 
 val add_class : typeclass -> unit
 
-val new_instance : typeclass -> int option -> bool -> constant -> instance
+val add_constant_class : constant -> unit
+
+val add_inductive_class : inductive -> unit
+
+val new_instance : typeclass -> int option -> bool -> global_reference -> instance
 val add_instance : instance -> unit
 
 val class_info : global_reference -> typeclass (* raises a UserError if not a class *)
@@ -61,11 +65,10 @@ 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 instance_impl : instance -> global_reference
 
 val is_class : global_reference -> bool
 val is_instance : global_reference -> bool
-val is_method : constant -> bool
 
 val is_implicit_arg : hole_kind -> bool
 
@@ -81,15 +84,17 @@ val bool_out : Dyn.t -> bool
 val is_resolvable : evar_info -> bool
 val mark_unresolvable : evar_info -> evar_info
 val mark_unresolvables : evar_map -> evar_map
-val is_class_evar : evar_info -> bool
+val is_class_evar : evar_map -> evar_info -> bool
 
-val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> 
-  env -> evar_defs -> evar_defs
-val resolve_one_typeclass : env -> evar_map -> types -> constr
+val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool ->
+  env -> evar_map -> evar_map
+val resolve_one_typeclass : env -> evar_map -> types -> open_constr
 
-val register_add_instance_hint : (constant -> int option -> unit) -> unit
-val add_instance_hint : constant -> int option -> unit
+val register_set_typeclass_transparency : (evaluable_global_reference -> bool -> unit) -> unit
+val set_typeclass_transparency : evaluable_global_reference -> bool -> unit
 
-val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> bool -> evar_defs) ref
-val solve_instanciation_problem : (env -> evar_map -> types -> constr) ref
+val register_add_instance_hint : (global_reference -> int option -> unit) -> unit
+val add_instance_hint : global_reference -> int option -> unit
 
+val solve_instanciations_problem : (env -> evar_map -> bool -> bool -> bool -> evar_map) ref
+val solve_instanciation_problem : (env -> evar_map -> types -> open_constr) ref
-- 
cgit v1.2.3