diff options
| author | Maxime Dénès | 2017-04-11 00:28:47 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-11 00:28:47 +0200 |
| commit | 835be3a05e28eb6e26f703a034f22b2c6c61acaa (patch) | |
| tree | 00ecf04840ba027c3c71f8503d9811c8a5dc1d2e /pretyping/classops.mli | |
| parent | 0980dbb1740c8d48d8ff0c516929f27f8cea854d (diff) | |
| parent | 2e6a89238dc7197057d0da80a16f4b4b1e41bfd8 (diff) | |
Merge PR#379: Introducing evar-insensitive constrs
Diffstat (limited to 'pretyping/classops.mli')
| -rw-r--r-- | pretyping/classops.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli index d509739cf4..0d741a5a5d 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -8,8 +8,9 @@ open Names open Term -open Evd open Environ +open EConstr +open Evd open Mod_subst (** {6 This is the type of class kinds } *) @@ -59,7 +60,7 @@ val class_info_from_index : cl_index -> cl_typ * cl_info_typ (** [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 +val find_class_type : evar_map -> types -> cl_typ * EInstance.t * constr list (** raises [Not_found] if not convertible to a class *) val class_of : env -> evar_map -> types -> types * cl_index @@ -104,7 +105,7 @@ val install_path_printer : val string_of_class : cl_typ -> string val pr_class : cl_typ -> std_ppcmds val pr_cl_index : cl_index -> std_ppcmds -val get_coercion_value : coe_index -> constr +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 |