Spracherkennung für: .in vermutete Sprache: Delphi {Delphi[73] CS[75] Ada[116]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
# TODO: Generate automatically with Dune
description = "The Coq Proof Assistant Plugin API"
version = "8.10"
directory = ""
requires = ""
package "config" (
description = "Coq Configuration Variables"
version = "8.10"
directory = "config"
archive(byte) = "config.cma"
archive(native) = "config.cmxa"
)
package "clib" (
description = "Base General Coq Library"
version = "8.10"
directory = "clib"
requires = "str, unix, threads"
archive(byte) = "clib.cma"
archive(native) = "clib.cmxa"
)
package "lib" (
description = "Base Coq-Specific Library"
version = "8.10"
directory = "lib"
requires = "coq.clib, coq.config, dynlink"
archive(byte) = "lib.cma"
archive(native) = "lib.cmxa"
)
package "vm" (
description = "Coq VM"
version = "8.10"
directory = "kernel/byterun"
# We could generate this file at configure time for the share byte
# build path to work properly.
#
# Enable this setting for local byte builds if you want dynamic linking:
#
# linkopts(byte) = "-dllpath path_to_coq/kernel/byterun/ -dllib -lcoqrun"
# We currently prefer static linking of the VM.
archive(byte) = "libcoqrun.a"
linkopts(byte) = "-custom"
)
package "kernel" (
description = "Coq's Kernel"
version = "8.10"
directory = "kernel"
requires = "coq.lib, coq.vm"
archive(byte) = "kernel.cma"
archive(native) = "kernel.cmxa"
)
package "library" (
description = "Coq Libraries (vo) support"
version = "8.10"
requires = "coq.kernel"
directory = "library"
archive(byte) = "library.cma"
archive(native) = "library.cmxa"
)
package "engine" (
description = "Coq Tactic Engine"
version = "8.10"
requires = "coq.library"
directory = "engine"
archive(byte) = "engine.cma"
archive(native) = "engine.cmxa"
)
package "pretyping" (
description = "Coq Pretyper"
version = "8.10"
requires = "coq.engine"
directory = "pretyping"
archive(byte) = "pretyping.cma"
archive(native) = "pretyping.cmxa"
)
package "interp" (
description = "Coq Term Interpretation"
version = "8.10"
requires = "coq.pretyping"
directory = "interp"
archive(byte) = "interp.cma"
archive(native) = "interp.cmxa"
)
package "proofs" (
description = "Coq Proof Engine"
version = "8.10"
requires = "coq.interp"
directory = "proofs"
archive(byte) = "proofs.cma"
archive(native) = "proofs.cmxa"
)
package "gramlib" (
description = "Coq Grammar Engine"
version = "8.10"
requires = "coq.lib"
directory = "gramlib/.pack"
archive(byte) = "gramlib.cma"
archive(native) = "gramlib.cmxa"
)
package "parsing" (
description = "Coq Parsing Engine"
version = "8.10"
requires = "coq.gramlib, coq.proofs"
directory = "parsing"
archive(byte) = "parsing.cma"
archive(native) = "parsing.cmxa"
)
package "printing" (
description = "Coq Printing Engine"
version = "8.10"
requires = "coq.parsing"
directory = "printing"
archive(byte) = "printing.cma"
archive(native) = "printing.cmxa"
)
package "tactics" (
description = "Coq Basic Tactics"
version = "8.10"
requires = "coq.printing"
directory = "tactics"
archive(byte) = "tactics.cma"
archive(native) = "tactics.cmxa"
)
package "vernac" (
description = "Coq Vernacular Interpreter"
version = "8.10"
requires = "coq.tactics"
directory = "vernac"
archive(byte) = "vernac.cma"
archive(native) = "vernac.cmxa"
)
package "stm" (
description = "Coq State Transactional Machine"
version = "8.10"
requires = "coq.vernac"
directory = "stm"
archive(byte) = "stm.cma"
archive(native) = "stm.cmxa"
)
package "toplevel" (
description = "Coq Toplevel"
version = "8.10"
requires = "num, coq.stm"
directory = "toplevel"
archive(byte) = "toplevel.cma"
archive(native) = "toplevel.cmxa"
)
package "idetop" (
description = "Coq IDE Libraries"
version = "8.10"
requires = "coq.toplevel"
directory = "ide"
archive(byte) = "coqidetop.cma"
archive(native) = "coqidetop.cmxa"
)
# XXX Depends on way less than toplevel
package "ide" (
description = "Coq IDE Libraries"
version = "8.10"
# XXX Add GTK
requires = "coq.toplevel"
directory = "ide"
archive(byte) = "ide.cma"
archive(native) = "ide.cmxa"
)
package "plugins" (
description = "Coq built-in plugins"
version = "8.10"
directory = "plugins"
package "ltac" (
description = "Coq LTAC Plugin"
version = "8.10"
requires = "coq.stm"
directory = "ltac"
archive(byte) = "ltac_plugin.cmo"
archive(native) = "ltac_plugin.cmx"
plugin(byte) = "ltac_plugin.cmo"
plugin(native) = "ltac_plugin.cmxs"
)
package "tauto" (
description = "Coq tauto plugin"
version = "8.10"
requires = "coq.plugins.ltac"
directory = "ltac"
archive(byte) = "tauto_plugin.cmo"
archive(native) = "tauto_plugin.cmx"
plugin(byte) = "tauto_plugin.cmo"
plugin(native) = "tauto_plugin.cmxs"
)
package "omega" (
description = "Coq omega plugin"
version = "8.10"
requires = "coq.plugins.ltac"
directory = "omega"
archive(byte) = "omega_plugin.cmo"
archive(native) = "omega_plugin.cmx"
plugin(byte) = "omega_plugin.cmo"
plugin(native) = "omega_plugin.cmxs"
)
package "micromega" (
description = "Coq micromega plugin"
version = "8.10"
requires = "num,coq.plugins.ltac"
directory = "micromega"
archive(byte) = "micromega_plugin.cmo"
archive(native) = "micromega_plugin.cmx"
plugin(byte) = "micromega_plugin.cmo"
plugin(native) = "micromega_plugin.cmxs"
)
package "setoid_ring" (
description = "Coq newring plugin"
version = "8.10"
requires = ""
directory = "setoid_ring"
archive(byte) = "newring_plugin.cmo"
archive(native) = "newring_plugin.cmx"
plugin(byte) = "newring_plugin.cmo"
plugin(native) = "newring_plugin.cmxs"
)
package "extraction" (
description = "Coq extraction plugin"
version = "8.10"
requires = "coq.plugins.ltac"
directory = "extraction"
archive(byte) = "extraction_plugin.cmo"
archive(native) = "extraction_plugin.cmx"
plugin(byte) = "extraction_plugin.cmo"
plugin(native) = "extraction_plugin.cmxs"
)
package "cc" (
description = "Coq cc plugin"
version = "8.10"
requires = "coq.plugins.ltac"
directory = "cc"
archive(byte) = "cc_plugin.cmo"
archive(native) = "cc_plugin.cmx"
plugin(byte) = "cc_plugin.cmo"
plugin(native) = "cc_plugin.cmxs"
)
package "firstorder" (
description = "Coq ground plugin"
version = "8.10"
requires = "coq.plugins.ltac"
directory = "firstorder"
archive(byte) = "ground_plugin.cmo"
archive(native) = "ground_plugin.cmx"
plugin(byte) = "ground_plugin.cmo"
plugin(native) = "ground_plugin.cmxs"
)
package "rtauto" (
description = "Coq rtauto plugin"
version = "8.10"
requires = "coq.plugins.ltac"
directory = "rtauto"
archive(byte) = "rtauto_plugin.cmo"
archive(native) = "rtauto_plugin.cmx"
plugin(byte) = "rtauto_plugin.cmo"
plugin(native) = "rtauto_plugin.cmxs"
)
package "btauto" (
description = "Coq btauto plugin"
version = "8.10"
requires = "coq.plugins.ltac"
directory = "btauto"
archive(byte) = "btauto_plugin.cmo"
archive(native) = "btauto_plugin.cmx"
plugin(byte) = "btauto_plugin.cmo"
plugin(native) = "btauto_plugin.cmxs"
)
package "funind" (
description = "Coq recdef plugin"
version = "8.10"
requires = "coq.plugins.extraction"
directory = "funind"
archive(byte) = "recdef_plugin.cmo"
archive(native) = "recdef_plugin.cmx"
plugin(byte) = "recdef_plugin.cmo"
plugin(native) = "recdef_plugin.cmxs"
)
package "nsatz" (
description = "Coq nsatz plugin"
version = "8.10"
requires = "num,coq.plugins.ltac"
directory = "nsatz"
archive(byte) = "nsatz_plugin.cmo"
archive(native) = "nsatz_plugin.cmx"
plugin(byte) = "nsatz_plugin.cmo"
plugin(native) = "nsatz_plugin.cmxs"
)
package "rsyntax" (
description = "Coq rsyntax plugin"
version = "8.10"
requires = ""
directory = "syntax"
archive(byte) = "r_syntax_plugin.cmo"
archive(native) = "r_syntax_plugin.cmx"
plugin(byte) = "r_syntax_plugin.cmo"
plugin(native) = "r_syntax_plugin.cmxs"
)
package "int63syntax" (
description = "Coq int63syntax plugin"
version = "8.10"
requires = ""
directory = "syntax"
archive(byte) = "int63_syntax_plugin.cmo"
archive(native) = "int63_syntax_plugin.cmx"
plugin(byte) = "int63_syntax_plugin.cmo"
plugin(native) = "int63_syntax_plugin.cmxs"
)
package "string_notation" (
description = "Coq string_notation plugin"
version = "8.10"
requires = ""
directory = "syntax"
archive(byte) = "string_notation_plugin.cmo"
archive(native) = "string_notation_plugin.cmx"
plugin(byte) = "string_notation_plugin.cmo"
plugin(native) = "string_notation_plugin.cmxs"
)
package "derive" (
description = "Coq derive plugin"
version = "8.10"
requires = ""
directory = "derive"
archive(byte) = "derive_plugin.cmo"
archive(native) = "derive_plugin.cmx"
plugin(byte) = "derive_plugin.cmo"
plugin(native) = "derive_plugin.cmxs"
)
package "ssrmatching" (
description = "Coq ssrmatching plugin"
version = "8.10"
requires = "coq.plugins.ltac"
directory = "ssrmatching"
archive(byte) = "ssrmatching_plugin.cmo"
archive(native) = "ssrmatching_plugin.cmx"
plugin(byte) = "ssrmatching_plugin.cmo"
plugin(native) = "ssrmatching_plugin.cmxs"
)
package "ssreflect" (
description = "Coq ssreflect plugin"
version = "8.10"
requires = "coq.plugins.ssrmatching"
directory = "ssr"
archive(byte) = "ssreflect_plugin.cmo"
archive(native) = "ssreflect_plugin.cmx"
plugin(byte) = "ssreflect_plugin.cmo"
plugin(native) = "ssreflect_plugin.cmxs"
)
)
[ Dauer der Verarbeitung: 0.62 Sekunden
]
