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/safe_typing.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/safe_typing.mli')

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