Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
889 B · 28 lines
at master
1234567891011121314151617181920212223242526272829# Comments in _CoqProject start with # and end with newline
# .v files in theories/ are modules whose name starts with "Tuto0"-R theories/ Tuto0
# META (an ocamlfind library specification) is necessary for rocq to find the plugin# in tuto0 we use rocq makefile's "-generate-meta-for-package"# it assumes that the plugin is called rocq-plugin-tutorial.plugin# and depends on ltac1 (rocq-runtime.plugins.ltac)# see tuto1 for an example of a custom META file-generate-meta-for-package rocq-plugin-tutorial
# rocq makefile uses -I to tell the ocaml compiler where previously compiled files are located# (in our case g_tuto0 depends on tuto0_main)-I src
# list our .v filestheories/Loader.vtheories/Demo.v
# list our ocaml filessrc/tuto0_main.mlsrc/tuto0_main.mlisrc/g_tuto0.mlg
# mlpack is a "rocq makefile" specific file# cf plugin tutorial READMEsrc/tuto0_plugin.mlpack