Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
601 B · 25 lines
at master
1234567891011121314151617181920212223242526META.rocq-plugin-tutorial-R theories Tuto1
# rocq makefile uses -I in 2 ways:# to tell rocq where the META file is located-I .# and to tell the ocaml compiler where previously compiled files are located# (eg g_tuto1 depends on inspector)-I src# in tuto0 with -generate-meta-for-package, the META was generated next to the mlpack# so -I src did both jobs
theories/Loader.vtheories/Demo.v
src/inspector.mlisrc/inspector.mlsrc/simple_check.mlisrc/simple_check.mlsrc/simple_declare.mlisrc/simple_declare.mlsrc/simple_print.mlsrc/simple_print.mlisrc/g_tuto1.mlgsrc/tuto1_plugin.mlpack