diff options
| author | Maxime Dénès | 2018-10-09 18:21:04 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-11-06 14:19:37 +0100 |
| commit | a1bdaf0635b5d5b9e007662f324dd526ba0fe8d3 (patch) | |
| tree | cc247d4ae7a66223add8ea189ca63125edd7d64e /kernel/indtypes.mli | |
| parent | 58f891c100d1a1821ed6385c1d06f9e0a77ecdac (diff) | |
[checker] Refactor by sharing code with the kernel
For historical reasons, the checker was duplicating a lot of code of the
kernel. The main differences I found were bug fixes that had not been
backported.
With this patch, the checker uses the kernel as a library to serve the
same purpose as before: validation of a `.vo` file, re-typechecking all
definitions a posteriori.
We also rename some files from the checker so that they don't clash with
kernel files.
Diffstat (limited to 'kernel/indtypes.mli')
| -rw-r--r-- | kernel/indtypes.mli | 13 |
1 files changed, 13 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 |