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.

1 files changed, 1 insertions, 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)