From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 pretyping/classops.mli | 22 +++-------------------
 1 file changed, 3 insertions(+), 19 deletions(-)

(limited to 'pretyping/classops.mli')

diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index f846a9e5..276b14d1 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: classops.mli,v 1.30.2.1 2004/07/16 19:30:44 herbelin Exp $ i*)
+(*i $Id: classops.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -15,6 +15,7 @@ open Term
 open Evd
 open Environ
 open Nametab
+open Mod_subst
 (*i*)
 
 (*s This is the type of class kinds *)
@@ -29,7 +30,6 @@ val subst_cl_typ : substitution -> cl_typ -> cl_typ
 
 (* This is the type of infos for declared classes *)
 type cl_info_typ = {
-  cl_strength : strength;
   cl_param : int }
 
 (* This is the type of coercion kinds *)
@@ -47,9 +47,6 @@ type coe_index
 (* This is the type of paths from a class to another *)
 type inheritance_path = coe_index list
 
-(*s [declare_class] adds a class to the set of declared classes *)
-val declare_class : cl_typ * strength * int -> unit
-
 (*s Access to classes infos *)
 val class_info : cl_typ -> (cl_index * cl_info_typ)
 val class_exists : cl_typ -> bool
@@ -69,7 +66,7 @@ val class_args_of : constr -> constr list
 
 (*s [declare_coercion] adds a coercion in the graph of coercion paths *)
 val declare_coercion : 
-  coe_typ -> unsafe_judgment -> strength -> isid:bool ->
+  coe_typ -> strength -> isid:bool ->
       src:cl_typ -> target:cl_typ -> params:int -> unit
 
 (*s Access to coercions infos *)
@@ -84,19 +81,6 @@ val lookup_path_to_sort_from : cl_index -> inheritance_path
 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
-
-open Libobject
-val inClass : (cl_typ * cl_info_typ) -> Libobject.obj
-val outClass : Libobject.obj -> (cl_typ * cl_info_typ)
-val inCoercion : coercion -> Libobject.obj
-val outCoercion : Libobject.obj -> coercion
-val coercion_strength : coe_info_typ -> strength
-val coercion_identity : coe_info_typ -> bool
-val coercion_params : coe_info_typ -> int
-(*i*)
-
 (*i Crade *)
 open Pp
 val install_path_printer : 
-- 
cgit v1.2.3