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(-)

(limited to 'checker')

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