4 files changed, 83 insertions, 19 deletions
diff --git a/doc/plugin_tutorial/tuto2/theories/Count.v b/doc/plugin_tutorial/tuto2/theories/Count.v
new file mode 100644
index 0000000000..3287342b75
--- /dev/null
+++ b/doc/plugin_tutorial/tuto2/theories/Count.v
@@ -0,0 +1,19 @@
+Require Import Demo.
+
+(*** Local ***)
+
+Count.
+Count.
+
+Import Demo.
+
+Count.
+
+(*** Persistent ***)
+
+Count Persistent.
+Count Persistent.
+
+Import Demo.
+
+Count Persistent.
diff --git a/doc/plugin_tutorial/tuto2/theories/Demo.v b/doc/plugin_tutorial/tuto2/theories/Demo.v
new file mode 100644
index 0000000000..73b5fcca62
--- /dev/null
+++ b/doc/plugin_tutorial/tuto2/theories/Demo.v
@@ -0,0 +1,63 @@
+From Tuto2 Require Import Loader.
+
+(*** A no-op command ***)
+
+Nothing.
+
+(*** No-op commands with arguments ***)
+
+(*
+ * Terminal parameters:
+ *)
+Command With Some Terminal Parameters.
+(* Command. *) (* does not parse *)
+
+(*
+ * A single non-terminal argument:
+ *)
+Pass 42.
+(* Pass. *) (* does not parse *)
+(* Pass True. *) (* does not parse *)
+(* Pass 15 20. *) (* does not parse *)
+
+(*
+ * A list of non-terminal arguments:
+ *)
+Accept 100 200 300 400.
+Accept.
+Accept 2.
+
+(*
+ * A custom argument:
+ *)
+Foobar Foo.
+Foobar Bar.
+
+(*** Commands that give feedback ***)
+
+(*
+ * Simple feedback:
+ *)
+Is Everything Awesome.
+
+(*** Storage and side effects ***)
+
+(*
+ * Local side effects:
+ *)
+Count.
+Count.
+Count.
+(*
+ * See Count.v for behavior in modules that import this one.
+ *)
+
+(*
+ * Persistent side effects:
+ *)
+Count Persistent.
+Count Persistent.
+Count Persistent.
+(*
+ * See Count.v for behavior in modules that import this one.
+ *)
diff --git a/doc/plugin_tutorial/tuto2/theories/Loader.v b/doc/plugin_tutorial/tuto2/theories/Loader.v
new file mode 100644
index 0000000000..9ce9991c86
--- /dev/null
+++ b/doc/plugin_tutorial/tuto2/theories/Loader.v
@@ -0,0 +1 @@
+Declare ML Module "tuto2_plugin".
diff --git a/doc/plugin_tutorial/tuto2/theories/Test.v b/doc/plugin_tutorial/tuto2/theories/Test.v
deleted file mode 100644
index 38e83bfff1..0000000000
--- a/doc/plugin_tutorial/tuto2/theories/Test.v
+++ /dev/null
@@ -1,19 +0,0 @@
-Declare ML Module "demo_plugin".
-
-Cmd1.
-Cmd2 With Some Terminal Parameters.
-Cmd3 42.
-Cmd4 100 200 300 400.
-Cmd5 Foo_5.
-Cmd5 Bar_5.
-Cmd6.
-Cmd7.
-Cmd7.
-Cmd7.
-
-Goal True.
-Proof.
-  tactic1.
-  tactic2 Foo_2.
-  tactic2 Bar_2.
-Abort.