Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
1.1 kB · 29 lines
at master
123456789101112131415161718192021222324252627282930# Comments in META start with # and end with newline
# our plugin is called rocq-plugin-tutorial.tuto1# rocq-plugin-tutorial from the META filename# tuto1 from this "package" namepackage "tuto1" ( # the plugin files are in "src" directory = "src"
version = "dev" description = "A tuto1 plugin"
# we define ltac1 tactics so we depend on ltac # otherwise we would depend only on rocq-runtime.vernac # (it contains the APIs for declaring new commands) # (ltac depends on vernac so if we depend on ltac, vernac is also implicitly depended on) requires = "rocq-runtime.plugins.ltac"
# the compiled plugin files (rocq makefile bases these filenames on the .mlpack filename) # (only the "plugin" keys are used by rocq, # "archive" is for packages which depend on this package) archive(byte) = "tuto1_plugin.cma" archive(native) = "tuto1_plugin.cmxa" plugin(byte) = "tuto1_plugin.cma" plugin(native) = "tuto1_plugin.cmxs")
# paths in this file are relative to this directorydirectory = "."