diff options
Diffstat (limited to 'tuto3/theories/Loader.v')
| -rw-r--r-- | tuto3/theories/Loader.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tuto3/theories/Loader.v b/tuto3/theories/Loader.v index eb3182cdaa..952565dbea 100644 --- a/tuto3/theories/Loader.v +++ b/tuto3/theories/Loader.v @@ -1,3 +1,3 @@ -From Tuto3 Require Import Data. +From Tuto3 Require Export Data. Declare ML Module "tuto3_plugin".
\ No newline at end of file |