From b5c0be9687aad69913e24354a041f188ee25efaf Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Tue, 1 May 2018 21:30:53 +0200
Subject: a first project on how to organize files and define a simple query

---
 tuto0/Makefile                | 14 ++++++++++++++
 tuto0/_CoqProject             |  5 +++++
 tuto0/src/g_tuto0.ml4         |  5 +++++
 tuto0/src/tuto0_plugin.mlpack |  1 +
 4 files changed, 25 insertions(+)
 create mode 100644 tuto0/Makefile
 create mode 100644 tuto0/_CoqProject
 create mode 100644 tuto0/src/g_tuto0.ml4
 create mode 100644 tuto0/src/tuto0_plugin.mlpack

diff --git a/tuto0/Makefile b/tuto0/Makefile
new file mode 100644
index 0000000000..e0e197650d
--- /dev/null
+++ b/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/tuto0/_CoqProject b/tuto0/_CoqProject
new file mode 100644
index 0000000000..2871fcd549
--- /dev/null
+++ b/tuto0/_CoqProject
@@ -0,0 +1,5 @@
+-R theories/ Tuto0
+-I src
+
+src/g_tuto0.ml4
+src/tuto0_plugin.mlpack
\ No newline at end of file
diff --git a/tuto0/src/g_tuto0.ml4 b/tuto0/src/g_tuto0.ml4
new file mode 100644
index 0000000000..5e0fa36e51
--- /dev/null
+++ b/tuto0/src/g_tuto0.ml4
@@ -0,0 +1,5 @@
+open Pp
+
+VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
+| [ "HelloWorld" ] -> [ Feedback.msg_notice (strbrk "Hello World!") ]
+END
\ No newline at end of file
diff --git a/tuto0/src/tuto0_plugin.mlpack b/tuto0/src/tuto0_plugin.mlpack
new file mode 100644
index 0000000000..9360e6036e
--- /dev/null
+++ b/tuto0/src/tuto0_plugin.mlpack
@@ -0,0 +1 @@
+G_tuto0
\ No newline at end of file
-- 
cgit v1.2.3