aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto0/theories/Loader.v
blob: 7bce38382b5e532584cc3dc5a4e10fae1bc763f6 (plain)
1
Declare ML Module "tuto0_plugin".