diff options
| -rw-r--r-- | checker/dune | 27 |
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) |