From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 pretyping/classops.mli | 24 +++++++++++++-----------
 1 file changed, 13 insertions(+), 11 deletions(-)

(limited to 'pretyping/classops.mli')

diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index f8600bbe..dc193c4e 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -21,7 +21,7 @@ type cl_typ =
   | CL_SECVAR of variable
   | CL_CONST of Constant.t
   | CL_IND of inductive
-  | CL_PROJ of Constant.t
+  | CL_PROJ of Projection.Repr.t
 
 (** Equality over [cl_typ] *)
 val cl_typ_eq : cl_typ -> cl_typ -> bool
@@ -36,19 +36,22 @@ type cl_info_typ = {
   cl_param : int }
 
 (** This is the type of coercion kinds *)
-type coe_typ = Globnames.global_reference
+type coe_typ = GlobRef.t
 
 (** This is the type of infos for declared coercions *)
-type coe_info_typ
+type coe_info_typ = {
+  coe_value : GlobRef.t;
+  coe_local : bool;
+  coe_is_identity : bool;
+  coe_is_projection : Projection.Repr.t option;
+  coe_param : int;
+}
 
 (** [cl_index] is the type of class keys *)
 type cl_index
 
-(** [coe_index] is the type of coercion keys *)
-type coe_index
-
 (** This is the type of paths from a class to another *)
-type inheritance_path = coe_index list
+type inheritance_path = coe_info_typ list
 
 (** {6 Access to classes infos } *)
 
@@ -79,8 +82,6 @@ val declare_coercion :
 (** {6 Access to coercions infos } *)
 val coercion_exists : coe_typ -> bool
 
-val coercion_value : coe_index -> (unsafe_judgment * bool * bool) Univ.in_universe_context_set
-
 (** {6 Lookup functions for coercion paths } *)
 
 (** @raise Not_found in the following functions when no path exists *)
@@ -105,11 +106,12 @@ val install_path_printer :
 val string_of_class : cl_typ -> string
 val pr_class : cl_typ -> Pp.t
 val pr_cl_index : cl_index -> Pp.t
-val get_coercion_value : coe_index -> Constr.t
 val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list
 val classes : unit -> cl_typ list
-val coercions : unit -> coe_index list
+val coercions : unit -> coe_info_typ list
 
 (** [hide_coercion] returns the number of params to skip if the coercion must
    be hidden, [None] otherwise; it raises [Not_found] if not a coercion *)
 val hide_coercion : coe_typ -> int option
+
+val is_coercion_in_scope : GlobRef.t -> bool
-- 
cgit v1.2.3