diff options
Diffstat (limited to 'pretyping/classops.mli')
| -rw-r--r-- | pretyping/classops.mli | 22 |
1 files changed, 3 insertions, 19 deletions
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 : |