1 files changed, 249 insertions, 0 deletions
diff --git a/META.coq b/META.coq
new file mode 100644
index 00000000..5be69d5f
--- /dev/null
+++ b/META.coq
@@ -0,0 +1,249 @@
+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"
+
+)