From 7f31b7f1ee4d4857aaed86ad7fd6bcbb83e2a705 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 17 May 2018 17:36:44 +0200
Subject: [tuto2] Clarify where the name of the ML plugin is used

---
 tuto2/_CoqProject            |  2 +-
 tuto2/src/demo.ml4           | 16 +++++++++++-----
 tuto2/src/demo_plugin.mlpack |  1 +
 tuto2/src/tuto_plugin.mlpack |  1 -
 tuto2/theories/Test.v        |  2 +-
 5 files changed, 14 insertions(+), 8 deletions(-)
 create mode 100644 tuto2/src/demo_plugin.mlpack
 delete mode 100644 tuto2/src/tuto_plugin.mlpack

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/demo_plugin.mlpack b/tuto2/src/demo_plugin.mlpack
new file mode 100644
index 0000000000..043a3b4633
--- /dev/null
+++ b/tuto2/src/demo_plugin.mlpack
@@ -0,0 +1 @@
+Demo
\ No newline at end of file
diff --git a/tuto2/src/tuto_plugin.mlpack b/tuto2/src/tuto_plugin.mlpack
deleted file mode 100644
index 043a3b4633..0000000000
--- a/tuto2/src/tuto_plugin.mlpack
+++ /dev/null
@@ -1 +0,0 @@
-Demo
\ No newline at end of file
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.
-- 
cgit v1.2.3