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.
---
 dev/checker_printers.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'dev/checker_printers.ml')

diff --git a/dev/checker_printers.ml b/dev/checker_printers.ml
index 40ae1a7b05..4f89bbd34e 100644
--- a/dev/checker_printers.ml
+++ b/dev/checker_printers.ml
@@ -59,15 +59,11 @@ let pP s = pp (hov 0 s)
 let ppuni u = pp(Universe.pr u)
 let ppuni_level u = pp (Level.pr u)
 
-let ppuniverse_set l = pp (LSet.pr l)
-let ppuniverse_instance l = pp (Instance.pr l)
-let ppauniverse_context l = pp (AUContext.pr Level.pr l)
 let ppuniverse_context l = pp (pr_universe_context Level.pr l)
 let ppconstraints c = pp (pr_constraints Level.pr c)
 let ppuniverse_context_future c =
   let ctx = Future.force c in
     ppuniverse_context ctx
-let ppuniverses u = pp (Univ.pr_universes u)
 
 let pploc x = let (l,r) = Loc.unloc x in
   print_string"(";print_int l;print_string",";print_int r;print_string")"
-- 
cgit v1.2.3