Imported Upstream version 8.5~beta1+dfsg

1 files changed, 19 insertions, 11 deletions

diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 0136b90c..c421b450 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -1,17 +1,15 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 open Names
-open Decl_kinds
 open Term
 open Evd
 open Environ
-open Nametab
 open Mod_subst
 
 (** {6 This is the type of class kinds } *)
@@ -21,6 +19,10 @@ type cl_typ =
   | CL_SECVAR of variable
   | CL_CONST of constant
   | CL_IND of inductive
+  | CL_PROJ of constant
+
+(** Equality over [cl_typ] *)
+val cl_typ_eq : cl_typ -> cl_typ -> bool
 
 val subst_cl_typ : substitution -> cl_typ -> cl_typ
 
@@ -29,7 +31,7 @@ type cl_info_typ = {
   cl_param : int }
 
 (** This is the type of coercion kinds *)
-type coe_typ = Libnames.global_reference
+type coe_typ = Globnames.global_reference
 
 (** This is the type of infos for declared coercions *)
 type coe_info_typ
@@ -44,13 +46,17 @@ type coe_index
 type inheritance_path = coe_index list
 
 (** {6 Access to classes infos } *)
-val class_info : cl_typ -> (cl_index * cl_info_typ)
+
 val class_exists : cl_typ -> bool
+
+val class_info : cl_typ -> (cl_index * cl_info_typ)
+(** @raise Not_found if this type is not a class *)
+
 val class_info_from_index : cl_index -> cl_typ * cl_info_typ
 
-(** [find_class_type env sigma c] returns the head reference of [c] and its
-   arguments *)
-val find_class_type : evar_map -> types -> cl_typ * constr list
+(** [find_class_type env sigma c] returns the head reference of [c],
+    its universe instance and its arguments *)
+val find_class_type : evar_map -> types -> cl_typ * Univ.universe_instance * constr list
 
 (** raises [Not_found] if not convertible to a class *)
 val class_of : env -> evar_map -> types -> types * cl_index
@@ -62,16 +68,18 @@ val class_args_of : env -> evar_map -> types -> constr list
 
 (** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *)
 val declare_coercion :
-  coe_typ -> locality -> isid:bool ->
+  coe_typ -> ?local:bool -> isid:bool ->
       src:cl_typ -> target:cl_typ -> params:int -> unit
 
 (** {6 Access to coercions infos } *)
 val coercion_exists : coe_typ -> bool
 
-val coercion_value : coe_index -> (unsafe_judgment * bool)
+val coercion_value : coe_index -> (unsafe_judgment * bool * bool) Univ.in_universe_context_set
 
 (** {6 Lookup functions for coercion paths } *)
+
 val lookup_path_between_class : cl_index * cl_index -> inheritance_path
+(** @raise Not_found when no such path exists *)
 
 val lookup_path_between : env -> evar_map -> types * types ->
       types * types * inheritance_path
@@ -80,7 +88,7 @@ val lookup_path_to_fun_from : env -> evar_map -> types ->
 val lookup_path_to_sort_from : env -> evar_map -> types ->
       types * inheritance_path
 val lookup_pattern_path_between :
-  inductive * inductive -> (constructor * int) list
+  env -> inductive * inductive -> (constructor * int) list
 
 (**/**)
 (* Crade *)