Tables logarithmiques pour les coercions + nettoyage

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

1 files changed, 5 insertions, 9 deletions

diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 50af9840c..aa0cca3dc 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -46,8 +46,6 @@ type coe_index
 (* This is the type of paths from a class to another *)
 type inheritance_path = coe_index list
 
-val coe_of_reference : Libnames.global_reference -> coe_typ
-
 (*s [declare_class] adds a class to the set of declared classes *)
 val declare_class : cl_typ * strength * int -> unit
 
@@ -77,7 +75,6 @@ val declare_coercion :
 
 (*s Access to coercions infos *)
 val coercion_exists : coe_typ -> bool
-val coercion_info_from_index : coe_index -> coe_typ * coe_info_typ
 
 val coercion_value : coe_index -> (unsafe_judgment * bool)
 
@@ -89,7 +86,7 @@ val lookup_pattern_path_between :
   cl_index * cl_index -> (constructor * int) list
 
 (*i Pour le discharge *)
-type coercion = (coe_typ * coe_info_typ) * cl_typ * cl_typ
+type coercion = coe_typ * coe_info_typ * cl_typ * cl_typ
 
 open Libobject
 val inClass : (cl_typ * cl_info_typ) -> Libobject.obj
@@ -109,13 +106,12 @@ val install_path_printer :
 
 (*s This is for printing purpose *)
 val string_of_class : cl_typ -> string
-val get_coercion_value : coe_info_typ -> constr
+val pr_class : cl_typ -> std_ppcmds
+val get_coercion_value : coe_index -> constr
 val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list
-val classes : unit -> (int * (cl_typ * cl_info_typ)) list
-val coercions : unit -> (int * (coe_typ * coe_info_typ)) list
+val classes : unit -> cl_typ list
+val coercions : unit -> coe_index 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
-
-