aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto1/theories/Loader.v
blob: 6e8e308b3f4a38197af224aa598ed404eb22abe3 (plain)
1
Declare ML Module "tuto1_plugin".