diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /pretyping/classops.mli | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'pretyping/classops.mli')
-rw-r--r-- | pretyping/classops.mli | 30 |
1 files changed, 19 insertions, 11 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 0136b90c..c421b450 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -1,17 +1,15 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Names -open Decl_kinds open Term open Evd open Environ -open Nametab open Mod_subst (** {6 This is the type of class kinds } *) @@ -21,6 +19,10 @@ type cl_typ = | CL_SECVAR of variable | CL_CONST of constant | CL_IND of inductive + | CL_PROJ of constant + +(** Equality over [cl_typ] *) +val cl_typ_eq : cl_typ -> cl_typ -> bool val subst_cl_typ : substitution -> cl_typ -> cl_typ @@ -29,7 +31,7 @@ type cl_info_typ = { cl_param : int } (** This is the type of coercion kinds *) -type coe_typ = Libnames.global_reference +type coe_typ = Globnames.global_reference (** This is the type of infos for declared coercions *) type coe_info_typ @@ -44,13 +46,17 @@ type coe_index type inheritance_path = coe_index list (** {6 Access to classes infos } *) -val class_info : cl_typ -> (cl_index * cl_info_typ) + val class_exists : cl_typ -> bool + +val class_info : cl_typ -> (cl_index * cl_info_typ) +(** @raise Not_found if this type is not a class *) + val class_info_from_index : cl_index -> cl_typ * cl_info_typ -(** [find_class_type env sigma c] returns the head reference of [c] and its - arguments *) -val find_class_type : evar_map -> types -> cl_typ * constr list +(** [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 (** raises [Not_found] if not convertible to a class *) val class_of : env -> evar_map -> types -> types * cl_index @@ -62,16 +68,18 @@ val class_args_of : env -> evar_map -> types -> constr list (** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *) val declare_coercion : - coe_typ -> locality -> isid:bool -> + coe_typ -> ?local:bool -> isid:bool -> src:cl_typ -> target:cl_typ -> params:int -> unit (** {6 Access to coercions infos } *) val coercion_exists : coe_typ -> bool -val coercion_value : coe_index -> (unsafe_judgment * bool) +val coercion_value : coe_index -> (unsafe_judgment * bool * bool) Univ.in_universe_context_set (** {6 Lookup functions for coercion paths } *) + val lookup_path_between_class : cl_index * cl_index -> inheritance_path +(** @raise Not_found when no such path exists *) val lookup_path_between : env -> evar_map -> types * types -> types * types * inheritance_path @@ -80,7 +88,7 @@ val lookup_path_to_fun_from : env -> evar_map -> types -> val lookup_path_to_sort_from : env -> evar_map -> types -> types * inheritance_path val lookup_pattern_path_between : - inductive * inductive -> (constructor * int) list + env -> inductive * inductive -> (constructor * int) list (**/**) (* Crade *) |