diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indtypes.mli | 13 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 4 |
3 files changed, 19 insertions, 0 deletions
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index cb09cfa827..a827c17683 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -34,6 +34,19 @@ type inductive_error = exception InductiveError of inductive_error +val infos_and_sort : env -> constr -> Univ.Universe.t + +val check_subtyping_arity_constructor : env -> (constr -> constr) -> types -> int -> bool -> unit + +val check_positivity : chkpos:bool -> + Names.MutInd.t -> + Environ.env -> + (Constr.constr, Constr.types) Context.Rel.pt -> + Declarations.recursivity_kind -> + ('a * Names.Id.t list * Constr.types array * + (('b, 'c) Context.Rel.pt * 'd)) + array -> Int.t * Declarations.recarg Rtree.t array + (** The following function does checks on inductive declarations. *) val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 4b64cc6d11..8b11851bbb 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1061,6 +1061,8 @@ type compiled_library = { comp_natsymbs : Nativecode.symbols } +let module_of_library lib = lib.comp_mod + type native_library = Nativecode.global list let get_library_native_symbols senv dir = diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 8fb33b04d4..7af773e3bc 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -141,6 +141,8 @@ val set_share_reduction : bool -> safe_transformer0 val set_VM : bool -> safe_transformer0 val set_native_compiler : bool -> safe_transformer0 +val check_engagement : Environ.env -> Declarations.set_predicativity -> unit + (** {6 Interactive module functions } *) val start_module : Label.t -> ModPath.t safe_transformer @@ -177,6 +179,8 @@ type compiled_library type native_library = Nativecode.global list +val module_of_library : compiled_library -> Declarations.module_body + val get_library_native_symbols : safe_environment -> DirPath.t -> Nativecode.symbols val start_library : DirPath.t -> ModPath.t safe_transformer |