9 files changed, 64 insertions, 0 deletions
diff --git a/doc/plugin_tutorial/tuto0/Makefile b/doc/plugin_tutorial/tuto0/Makefile
new file mode 100644
index 0000000000..e0e197650d
--- /dev/null
+++ b/doc/plugin_tutorial/tuto0/Makefile
@@ -0,0 +1,14 @@
+ifeq "$(COQBIN)" ""
+  COQBIN=$(dir $(shell which coqtop))/
+endif
+
+%: Makefile.coq
+
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
+
+tests: all
+	@$(MAKE) -C tests -s clean
+	@$(MAKE) -C tests -s all
+
+-include Makefile.coq
diff --git a/doc/plugin_tutorial/tuto0/_CoqProject b/doc/plugin_tutorial/tuto0/_CoqProject
new file mode 100644
index 0000000000..76368e3ac7
--- /dev/null
+++ b/doc/plugin_tutorial/tuto0/_CoqProject
@@ -0,0 +1,10 @@
+-R theories/ Tuto0
+-I src
+
+theories/Loader.v
+theories/Demo.v
+
+src/tuto0_main.ml
+src/tuto0_main.mli
+src/g_tuto0.mlg
+src/tuto0_plugin.mlpack
diff --git a/doc/plugin_tutorial/tuto0/src/dune b/doc/plugin_tutorial/tuto0/src/dune
new file mode 100644
index 0000000000..79d561061d
--- /dev/null
+++ b/doc/plugin_tutorial/tuto0/src/dune
@@ -0,0 +1,9 @@
+(library
+ (name tuto0_plugin)
+ (public_name coq.plugins.tutorial.p0)
+ (libraries coq.plugins.ltac))
+
+(rule
+ (targets g_tuto0.ml)
+ (deps (:pp-file g_tuto0.mlg) )
+ (action (run coqpp %{pp-file})))
diff --git a/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg b/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg
new file mode 100644
index 0000000000..5c633fe862
--- /dev/null
+++ b/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg
@@ -0,0 +1,18 @@
+DECLARE PLUGIN "tuto0_plugin"
+
+{
+
+open Pp
+open Ltac_plugin
+
+}
+
+VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
+| [ "HelloWorld" ] -> { Feedback.msg_notice (strbrk Tuto0_main.message) }
+END
+
+TACTIC EXTEND hello_world_tactic
+| [ "hello_world" ] ->
+  { let _ = Feedback.msg_notice (str Tuto0_main.message) in
+    Tacticals.New.tclIDTAC }
+END
diff --git a/doc/plugin_tutorial/tuto0/src/tuto0_main.ml b/doc/plugin_tutorial/tuto0/src/tuto0_main.ml
new file mode 100644
index 0000000000..93a807a800
--- /dev/null
+++ b/doc/plugin_tutorial/tuto0/src/tuto0_main.ml
@@ -0,0 +1 @@
+let message = "Hello world!"
diff --git a/doc/plugin_tutorial/tuto0/src/tuto0_main.mli b/doc/plugin_tutorial/tuto0/src/tuto0_main.mli
new file mode 100644
index 0000000000..846af3ed8c
--- /dev/null
+++ b/doc/plugin_tutorial/tuto0/src/tuto0_main.mli
@@ -0,0 +1 @@
+val message : string
diff --git a/doc/plugin_tutorial/tuto0/src/tuto0_plugin.mlpack b/doc/plugin_tutorial/tuto0/src/tuto0_plugin.mlpack
new file mode 100644
index 0000000000..73be1bb561
--- /dev/null
+++ b/doc/plugin_tutorial/tuto0/src/tuto0_plugin.mlpack
@@ -0,0 +1,2 @@
+Tuto0_main
+G_tuto0
diff --git a/doc/plugin_tutorial/tuto0/theories/Demo.v b/doc/plugin_tutorial/tuto0/theories/Demo.v
new file mode 100644
index 0000000000..bdc61986af
--- /dev/null
+++ b/doc/plugin_tutorial/tuto0/theories/Demo.v
@@ -0,0 +1,8 @@
+From Tuto0 Require Import Loader.
+
+HelloWorld.
+
+Lemma test : True.
+Proof.
+hello_world.
+Abort.
diff --git a/doc/plugin_tutorial/tuto0/theories/Loader.v b/doc/plugin_tutorial/tuto0/theories/Loader.v
new file mode 100644
index 0000000000..7bce38382b
--- /dev/null
+++ b/doc/plugin_tutorial/tuto0/theories/Loader.v
@@ -0,0 +1 @@
+Declare ML Module "tuto0_plugin".