From a1bdaf0635b5d5b9e007662f324dd526ba0fe8d3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 9 Oct 2018 18:21:04 +0200
Subject: [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.
---
 kernel/indtypes.mli | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'kernel/indtypes.mli')

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
-- 
cgit v1.2.3