description = "The Coq Proof Assistant Plugin API"
version = "8.6"
directory = ""
requires = "camlp5"
package "config" (
description = "Coq Configuration Variables"
version = "8.6"
directory = "config"
)
package "lib" (
description = "Base Coq Library"
version = "8.6"
directory = "lib"
requires = "coq.config"
archive(byte) = "clib.cma"
archive(byte) += "lib.cma"
archive(native) = "clib.cmxa"
archive(native) += "lib.cmxa"
)
package "vm" (
description = "Coq VM"
version = "8.6"
# EJGA FIXME: Unfortunately dllpath is dependent on the type of Coq
# install. In a local one we'll want kernel/byterun, in a non-local
# one we want to set it to coqlib. We should thus generate this file
# at configure time, but let's hear for some more feedback from
# experts.
# Enable for local native & byte builds
# directory = "kernel/byterun"
# Enable for local byte builds and set up properly
# linkopts(byte) = "-dllpath /path/to/coq/kernel/byterun/ -dllib -lcoqrun"
# Disable for local byte builds
linkopts(byte) = "-dllib -lcoqrun"
linkopts(native) = "-cclib -lcoqrun"
)
package "kernel" (
description = "The Coq's Kernel"
version = "8.6"
directory = "kernel"
requires = "coq.lib, coq.vm"
archive(byte) = "kernel.cma"
archive(native) = "kernel.cmxa"
)
package "library" (
description = "Coq Libraries (vo) support"
version = "8.6"
requires = "coq.kernel"
directory = "library"
archive(byte) = "library.cma"
archive(native) = "library.cmxa"
)
package "intf" (
description = "Coq Public Data Types"
version = "8.6"
requires = "coq.library"
directory = "intf"
)
package "engine" (
description = "Coq Libraries (vo) support"
version = "8.6"
requires = "coq.library"
directory = "engine"
archive(byte) = "engine.cma"
archive(native) = "engine.cmxa"
)
package "pretyping" (
description = "Coq Pretyper"
version = "8.6"
requires = "coq.engine"
directory = "pretyping"
archive(byte) = "pretyping.cma"
archive(native) = "pretyping.cmxa"
)
package "interp" (
description = "Coq Term Interpretation"
version = "8.6"
requires = "coq.pretyping"
directory = "interp"
archive(byte) = "interp.cma"
archive(native) = "interp.cmxa"
)
package "grammar" (
description = "Coq Base Grammar"
version = "8.6"
requires = "coq.interp"
directory = "grammar"
archive(byte) = "grammar.cma"
archive(native) = "grammar.cmxa"
)
package "proofs" (
description = "Coq Proof Engine"
version = "8.6"
requires = "coq.interp"
directory = "proofs"
archive(byte) = "proofs.cma"
archive(native) = "proofs.cmxa"
)
package "parsing" (
description = "Coq Parsing Engine"
version = "8.6"
requires = "coq.proofs"
directory = "parsing"
archive(byte) = "parsing.cma"
archive(native) = "parsing.cmxa"
)
package "printing" (
description = "Coq Printing Libraries"
version = "8.6"
requires = "coq.parsing"
directory = "printing"
archive(byte) = "printing.cma"
archive(native) = "printing.cmxa"
)
package "tactics" (
description = "Coq Tactics"
version = "8.6"
requires = "coq.printing"
directory = "tactics"
archive(byte) = "tactics.cma"
archive(native) = "tactics.cmxa"
)
package "stm" (
description = "Coq State Transactional Machine"
version = "8.6"
requires = "coq.tactics"
directory = "stm"
archive(byte) = "stm.cma"
archive(native) = "stm.cmxa"
)
package "toplevel" (
description = "Coq Toplevel"
version = "8.6"
requires = "coq.stm"
directory = "toplevel"
archive(byte) = "toplevel.cma"
archive(native) = "toplevel.cmxa"
)
package "highparsing" (
description = "Coq Extra Parsing"
version = "8.6"
requires = "coq.toplevel"
directory = "parsing"
archive(byte) = "highparsing.cma"
archive(native) = "highparsing.cmxa"
)
package "ltac" (
description = "Coq LTAC Plugin"
version = "8.6"
requires = "coq.highparsing"
directory = "ltac"
archive(byte) = "ltac.cma"
archive(native) = "ltac.cmxa"
)