diff options
Diffstat (limited to 'kernel/typeops.mli')
| -rw-r--r-- | kernel/typeops.mli | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli index e61d5c399e..87a5666fcc 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -94,8 +94,9 @@ val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment (** {6 Type of Cases. } *) val judge_of_case : env -> case_info - -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array - -> unsafe_judgment + -> unsafe_judgment -> (constr,Instance.t) case_invert -> unsafe_judgment + -> unsafe_judgment array + -> unsafe_judgment (** {6 Type of global references. } *) @@ -113,8 +114,6 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) -> GlobRef.t -> Constr.named_context -> unit -val check_primitive_type : env -> CPrimitives.op_or_type -> types -> unit - (** Types for primitives *) val type_of_int : env -> types @@ -123,8 +122,16 @@ val judge_of_int : env -> Uint63.t -> unsafe_judgment val type_of_float : env -> types val judge_of_float : env -> Float64.t -> unsafe_judgment -val type_of_prim_type : env -> CPrimitives.prim_type -> types -val type_of_prim : env -> CPrimitives.t -> types +val type_of_array : env -> Univ.Instance.t -> types +val judge_of_array : env -> Univ.Instance.t -> unsafe_judgment array -> unsafe_judgment -> unsafe_judgment + +val type_of_prim_type : env -> Univ.Instance.t -> 'a CPrimitives.prim_type -> types +val type_of_prim : env -> Univ.Instance.t -> CPrimitives.t -> types +val type_of_prim_or_type : env -> Univ.Instance.t -> CPrimitives.op_or_type -> types val warn_bad_relevance_name : string (** Allow the checker to make this warning into an error. *) + +val should_invert_case : env -> case_info -> bool +(** We have case inversion exactly when going from irrelevant nonempty + (ie 1 constructor) inductive to relevant type. *) |