From d7172fbf2d7ae98ea0471a58c21f93671280d50e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 9 Nov 2018 19:27:37 +0100
Subject: Fix dune-dbg using checker/main -> checker/coqchk

---
 dev/dune        | 2 +-
 dev/dune-dbg.in | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/dev/dune b/dev/dune
index bfa2d525c9..29a20ac17f 100644
--- a/dev/dune
+++ b/dev/dune
@@ -9,7 +9,7 @@
 (rule
   (targets dune-dbg)
   (deps dune-dbg.in
-        ../checker/main.bc
+        ../checker/coqchk.bc
         ../topbin/coqtop_byte_bin.bc
         ; This is not enough as the call to `ocamlfind` will fail :/
         top_printers.cma)
diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in
index 3f3df23fe1..80ad0500e0 100755
--- a/dev/dune-dbg.in
+++ b/dev/dune-dbg.in
@@ -3,7 +3,7 @@
 # Run in a proper install dune env.
 case $1 in
     checker)
-        exe=_build/default/checker/main.bc
+        exe=_build/default/checker/coqchk.bc
         ;;
     *)
         exe=_build/default/topbin/coqtop_byte_bin.bc
-- 
cgit v1.2.3


From 7aeddf5cbf5755dab1cdcbab832c3d51a02c6c84 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 9 Nov 2018 19:28:14 +0100
Subject: dune: link kernel in checker instead of copying files

This allows to use the nice printers with constrextern etc, and since
we were copying everything we're not linking any more than previously.

Also the dune file is simpler without the copies.
---
 checker/dune | 27 +--------------------------
 1 file changed, 1 insertion(+), 26 deletions(-)

diff --git a/checker/dune b/checker/dune
index 3ab4f50d13..ee427d26c5 100644
--- a/checker/dune
+++ b/checker/dune
@@ -1,26 +1,3 @@
-(copy_files#
-  %{project_root}/kernel/{names,esubst,declarations,environ,constr,term,univ,evar,sorts,uGraph,context}.ml{,i})
-
-(copy_files#
-  %{project_root}/kernel/{mod_subst,vars,opaqueproof,conv_oracle,reduction,typeops,inductive,indtypes,declareops,type_errors}.ml{,i})
-
-(copy_files#
-  %{project_root}/kernel/{modops,mod_typing,}.ml{,i})
-
-(copy_files#
-  %{project_root}/kernel/{cClosure,cPrimitives,csymtable,vconv,vm,uint31,cemitcodes,vmvalues,cbytecodes,cinstr,retroknowledge,copcodes}.ml{,i})
-
-(copy_files#
-  %{project_root}/kernel/{cbytegen,clambda,nativeinstr,nativevalues,nativeconv,nativecode,nativelib,nativelibrary,nativelambda}.ml{,i})
-
-(copy_files#
-  %{project_root}/kernel/{subtyping,term_typing,safe_typing,entries,cooking,transparentState}.ml{,i})
-
-; VM stuff
-
-(copy_files#
-  %{project_root}/kernel/byterun/{*.c,*.h})
-
 ; Careful with bug https://github.com/ocaml/odoc/issues/148
 ;
 ; If we don't pack checker we will have a problem here due to
@@ -30,10 +7,8 @@
  (public_name coq.checklib)
  (synopsis "Coq's Standalone Proof Checker")
  (modules :standard \ coqchk votour)
- (modules_without_implementation cinstr nativeinstr)
- (c_names coq_fix_code coq_memory coq_values coq_interp)
  (wrapped true)
- (libraries coq.lib))
+ (libraries coq.kernel))
 
 (executable
  (name coqchk)
-- 
cgit v1.2.3