Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/doc/plugin_tutorial/tuto1/   (Beweissystem des Inria Version 9.1.0©)  Datei vom 15.8.2025 mit Größe 601 B image not shown  

Quelle  _CoqProject   Sprache: unbekannt

 
META.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.v
theories/Demo.v

src/inspector.mli
src/inspector.ml
src/simple_check.mli
src/simple_check.ml
src/simple_declare.mli
src/simple_declare.ml
src/simple_print.ml
src/simple_print.mli
src/g_tuto1.mlg
src/tuto1_plugin.mlpack

97%


[ Dauer der Verarbeitung: 0.14 Sekunden  (vorverarbeitet)  ]