diff options
| author | Enrico Tassi | 2018-05-17 17:36:44 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-05-17 17:38:13 +0200 |
| commit | 7f31b7f1ee4d4857aaed86ad7fd6bcbb83e2a705 (patch) | |
| tree | 79b805c1e2210ab957f2f3596ecc6d07a977dd2e | |
| parent | 679140212d704885f91ec4a23d60628f85bf830a (diff) | |
[tuto2] Clarify where the name of the ML plugin is used
| -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. |