diff options
| author | Pierre-Marie Pédrot | 2018-11-21 13:06:23 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-21 13:06:23 +0100 |
| commit | e0db7f1baef37bb60db2dd1c963572f175392783 (patch) | |
| tree | 8fc59a2d77d5cd32622c5a4f2071d22abee5a78f /checker | |
| parent | 4d0fea2ededb11d79f4f1abcc1595f9cec20d6dd (diff) | |
| parent | 7aeddf5cbf5755dab1cdcbab832c3d51a02c6c84 (diff) | |
Merge PR #8961: dune: link kernel in checker instead of copying files
Diffstat (limited to 'checker')
| -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) |