From 0fe2b5d4d63bcbc63d48a386949094c23e4c274e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 31 Oct 2018 17:57:47 +0100
Subject: Port to coqpp.

---
 tuto0/_CoqProject     |  2 +-
 tuto0/src/g_tuto0.ml4 | 14 --------------
 tuto0/src/g_tuto0.mlg | 18 ++++++++++++++++++
 3 files changed, 19 insertions(+), 15 deletions(-)
 delete mode 100644 tuto0/src/g_tuto0.ml4
 create mode 100644 tuto0/src/g_tuto0.mlg

(limited to 'tuto0')

diff --git a/tuto0/_CoqProject b/tuto0/_CoqProject
index dd93e1fa79..76368e3ac7 100644
--- a/tuto0/_CoqProject
+++ b/tuto0/_CoqProject
@@ -6,5 +6,5 @@ theories/Demo.v
 
 src/tuto0_main.ml
 src/tuto0_main.mli
-src/g_tuto0.ml4
+src/g_tuto0.mlg
 src/tuto0_plugin.mlpack
diff --git a/tuto0/src/g_tuto0.ml4 b/tuto0/src/g_tuto0.ml4
deleted file mode 100644
index d6e95ba0f7..0000000000
--- a/tuto0/src/g_tuto0.ml4
+++ /dev/null
@@ -1,14 +0,0 @@
-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/tuto0/src/g_tuto0.mlg b/tuto0/src/g_tuto0.mlg
new file mode 100644
index 0000000000..5c633fe862
--- /dev/null
+++ b/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
-- 
cgit v1.2.3