diff options
| author | Yves Bertot | 2018-05-17 21:54:49 +0200 |
|---|---|---|
| committer | GitHub | 2018-05-17 21:54:49 +0200 |
| commit | 35b4f622a118cccf5e8dd961dd75b31c3ea9e5fd (patch) | |
| tree | f339da33904b102439174067ed4bff1d58394415 | |
| parent | 0cb5498b54940167607d39c5a266cca21a3657ca (diff) | |
| parent | 7f31b7f1ee4d4857aaed86ad7fd6bcbb83e2a705 (diff) | |
Merge pull request #5 from gares/fix/tuto2
[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. |