; Dune doesn't use configure's output, but it is still necessary for
; some Coq files to work; will be fixed in the future.
(rule
 (targets dune.c_flags)
 (mode fallback)
 (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX))
 (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no))))

(env
 (dev     (c_flags (:include dune.c_flags)))
 (release (c_flags (:include dune.c_flags)))
 (ireport (c_flags (:include dune.c_flags))))

(library
 (name byterun)
 (synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]")
 (public_name coq.vm)
 (c_names coq_fix_code coq_memory coq_values coq_interp))

(rule
 (targets coq_instruct.h)
 (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe enum))))

(rule
 (targets coq_jumptbl.h)
 (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe jump))))