diff options
| -rw-r--r-- | tuto2/_CoqProject | 2 | ||||
| -rw-r--r-- | tuto2/src/demo.ml4 | 16 | ||||
| -rw-r--r-- | tuto2/src/demo_plugin.mlpack (renamed from tuto2/src/tuto_plugin.mlpack) | 0 | ||||
| -rw-r--r-- | tuto2/theories/Test.v | 2 |
4 files changed, 13 insertions, 7 deletions
diff --git a/tuto2/_CoqProject b/tuto2/_CoqProject index f38ee8d6a6..bdafdb5f04 100644 --- a/tuto2/_CoqProject +++ b/tuto2/_CoqProject @@ -3,4 +3,4 @@ theories/Test.v src/demo.ml4 -src/tuto_plugin.mlpack +src/demo_plugin.mlpack diff --git a/tuto2/src/demo.ml4 b/tuto2/src/demo.ml4 index 3d165a6302..981d41fa5c 100644 --- a/tuto2/src/demo.ml4 +++ b/tuto2/src/demo.ml4 @@ -4,23 +4,29 @@ (* *) (* -------------------------------------------------------------------------- *) -DECLARE PLUGIN "demo" +DECLARE PLUGIN "demo_plugin" (* - Use this macro before any of the other Ocaml macros. + Use this macro before any of the other OCaml macros. Each plugin has a unique name. - We have decided to name this plugin as "demo". + We have decided to name this plugin as "demo_plugin". That means that: (1) If we want to load this particular plugin to Coq toplevel, we must use the following command. - Declare ML Module "demo". + Declare ML Module "demo_plugin". - (2) The above command will succeed only if there is "demo.cmxs" + (2) The above command will succeed only if there is "demo_plugin.cmxs" in some of the directories that Coq is supposed to look (i.e. the ones we specified via "-I ..." command line options). + + (3) The file "demo_plugin.mlpack" lists the OCaml modules to be linked in + "demo_plugin.cmxs". + + (4) The file "demo_plugin.mlpack" as well as all .ml, .mli and .ml4 files + are listed in the "_CoqProject" file. *) (* -------------------------------------------------------------------------- *) diff --git a/tuto2/src/tuto_plugin.mlpack b/tuto2/src/demo_plugin.mlpack index 043a3b4633..043a3b4633 100644 --- a/tuto2/src/tuto_plugin.mlpack +++ b/tuto2/src/demo_plugin.mlpack diff --git a/tuto2/theories/Test.v b/tuto2/theories/Test.v index 5522a3444a..38e83bfff1 100644 --- a/tuto2/theories/Test.v +++ b/tuto2/theories/Test.v @@ -1,4 +1,4 @@ -Declare ML Module "demo". +Declare ML Module "demo_plugin". Cmd1. Cmd2 With Some Terminal Parameters. |