[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.

3 files changed, 21 insertions, 45 deletions

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")"
diff --git a/dev/checker_printers.mli b/dev/checker_printers.mli
index 2f9500c5c3..8be9b87257 100644
--- a/dev/checker_printers.mli
+++ b/dev/checker_printers.mli
@@ -43,12 +43,8 @@ val ppididmap : Names.Id.t Names.Id.Map.t -> unit
 (* Universes *)
 val ppuni : Univ.Universe.t -> unit
 val ppuni_level : Univ.Level.t -> unit (* raw *)
-val ppuniverse_set : Univ.LSet.t -> unit
-val ppuniverse_instance : Univ.Instance.t -> unit
-val ppauniverse_context : Univ.AUContext.t -> unit
 val ppuniverse_context : Univ.UContext.t -> unit
 val ppconstraints : Univ.Constraint.t -> unit
 val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit
-val ppuniverses : Univ.universes -> unit
 
 val pploc : Loc.t -> unit
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 85bb04efe0..d330f517be 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -14,40 +14,24 @@
 
 export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH
 
-GUESS_CHECKER=
-for arg in "$@"; do
-    if [ "${arg##*/}" = coqchk.byte ]; then
-        GUESS_CHECKER=1
-    fi
-done
-
-if [ -z "$GUESS_CHECKER" ]; then
-    exec $OCAMLDEBUG \
-	-I $CAMLP5LIB -I +threads \
-	-I $COQTOP \
-	-I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \
-	-I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
-	-I $COQTOP/library -I $COQTOP/engine \
-	-I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \
-        -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
-	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \
-        -I $COQTOP/plugins/cc         -I $COQTOP/plugins/dp \
-        -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \
-        -I $COQTOP/plugins/firstorder \
-        -I $COQTOP/plugins/funind     -I $COQTOP/plugins/groebner \
-        -I $COQTOP/plugins/interface  -I $COQTOP/plugins/micromega \
-        -I $COQTOP/plugins/omega      -I $COQTOP/plugins/quote \
-        -I $COQTOP/plugins/ring \
-	-I $COQTOP/plugins/rtauto     -I $COQTOP/plugins/setoid_ring \
-        -I $COQTOP/plugins/subtac     -I $COQTOP/plugins/syntax \
-        -I $COQTOP/plugins/xml        -I $COQTOP/plugins/ltac \
-        -I $COQTOP/ide \
-	"$@"
-else
-    exec $OCAMLDEBUG \
-        -I $CAMLP5LIB -I +threads \
-        -I $COQTOP \
-        -I $COQTOP/config -I $COQTOP/clib \
-        -I $COQTOP/lib -I $COQTOP/checker \
-        "$@"
-fi
+exec $OCAMLDEBUG \
+    -I $CAMLP5LIB -I +threads \
+    -I $COQTOP \
+    -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \
+    -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
+    -I $COQTOP/library -I $COQTOP/engine \
+    -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \
+    -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
+    -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \
+    -I $COQTOP/plugins/cc         -I $COQTOP/plugins/dp \
+    -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \
+    -I $COQTOP/plugins/firstorder \
+    -I $COQTOP/plugins/funind     -I $COQTOP/plugins/groebner \
+    -I $COQTOP/plugins/interface  -I $COQTOP/plugins/micromega \
+    -I $COQTOP/plugins/omega      -I $COQTOP/plugins/quote \
+    -I $COQTOP/plugins/ring \
+    -I $COQTOP/plugins/rtauto     -I $COQTOP/plugins/setoid_ring \
+    -I $COQTOP/plugins/subtac     -I $COQTOP/plugins/syntax \
+    -I $COQTOP/plugins/xml        -I $COQTOP/plugins/ltac \
+    -I $COQTOP/ide \
+    "$@"