1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
(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}.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
; duplicate module names in the whole build.
(library
(name checklib)
(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))
(executable
(name coqchk)
(public_name coqchk)
(package coq)
(modules coqchk)
(flags :standard -open Checklib)
(libraries coq.checklib))
(executable
(name votour)
(public_name votour)
(package coq)
(modules votour)
(flags :standard -open Checklib)
(libraries coq.checklib))
|
