doc/plugin_tutorial/tuto1/src · coq · Tangled

forked from coq/coq

coq doc plugin_tutorial tuto1 src

11 files

Suraaj K S · Fix reference to stdarg.mli in documentation · 9mo ago

Use `rocq pp-mlg` for rocq-runtime files, move `coqpp` back to `coq-core`

Fix reference to stdarg.mli in documentation

Clean, document, and expand plugin tutorials 0 and 1

Clean, document, and expand plugin tutorials 0 and 1

simple_check.ml

Clean, document, and expand plugin tutorials 0 and 1

simple_check.mli

Clean, document, and expand plugin tutorials 0 and 1

simple_declare.ml

Reduce explicit use of default definition scope

simple_declare.mli

Introduce PolyFlags to gather flags for polymorphic defs

simple_print.ml

Use vernactypes to get indirect accessor in commands

simple_print.mli

Use vernactypes to get indirect accessor in commands

tuto1_plugin.mlpack

Clean, document, and expand plugin tutorials 0 and 1