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.

---
 tuto3/_CoqProject     |  4 ++--
 tuto3/src/g_tuto3.ml4 | 42 ------------------------------------------
 tuto3/src/g_tuto3.mlg | 46 ++++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 48 insertions(+), 44 deletions(-)
 delete mode 100644 tuto3/src/g_tuto3.ml4
 create mode 100644 tuto3/src/g_tuto3.mlg

(limited to 'tuto3')

diff --git a/tuto3/_CoqProject b/tuto3/_CoqProject
index 6a3c1978a7..e2a60a430f 100644
--- a/tuto3/_CoqProject
+++ b/tuto3/_CoqProject
@@ -8,5 +8,5 @@ src/tuto_tactic.ml
 src/tuto_tactic.mli
 src/construction_game.ml
 src/construction_game.mli
-src/g_tuto3.ml4
-src/tuto3_plugin.mlpack
\ No newline at end of file
+src/g_tuto3.mlg
+src/tuto3_plugin.mlpack
diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.ml4
deleted file mode 100644
index 71c6be16c8..0000000000
--- a/tuto3/src/g_tuto3.ml4
+++ /dev/null
@@ -1,42 +0,0 @@
-DECLARE PLUGIN "tuto3_plugin"
-
-open Ltac_plugin
-
-open Construction_game
-
-(* This one is necessary, to avoid message about missing wit_string *)
-open Stdarg
-
-VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY
-| [ "Tuto3_1" ] ->
-  [ let env = Global.env () in
-    let evd = Evd.from_env env in
-    let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in
-    let new_type_2 = EConstr.mkSort s in
-    let evd, _ =
-      Typing.type_of (Global.env()) (Evd.from_env (Global.env())) new_type_2 in
-    Feedback.msg_notice
-      (Printer.pr_econstr_env env evd new_type_2) ]
-END
-
-VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
-| [ "Tuto3_2" ] -> [ example_sort_app_lambda () ]
-END
-
-TACTIC EXTEND collapse_hyps
-| [ "pack" "hypothesis" ident(i) ] ->
-  [ Tuto_tactic.pack_tactic i ]
-END
-
-(* More advanced examples, where automatic proof happens but
-   no tactic is being called explicitely.  The first one uses
-   type classes. *)
-VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
-| [ "Tuto3_3" int(n) ] -> [ example_classes n ]
-END
-
-(* The second one uses canonical structures. *)
-VERNAC COMMAND EXTEND TriggerCanonical CLASSIFIED AS QUERY
-| [ "Tuto3_4" int(n) ] -> [ example_canonical n ]
-END
-
diff --git a/tuto3/src/g_tuto3.mlg b/tuto3/src/g_tuto3.mlg
new file mode 100644
index 0000000000..82ba45726e
--- /dev/null
+++ b/tuto3/src/g_tuto3.mlg
@@ -0,0 +1,46 @@
+DECLARE PLUGIN "tuto3_plugin"
+
+{
+
+open Ltac_plugin
+
+open Construction_game
+
+(* This one is necessary, to avoid message about missing wit_string *)
+open Stdarg
+
+}
+
+VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY
+| [ "Tuto3_1" ] ->
+  { let env = Global.env () in
+    let evd = Evd.from_env env in
+    let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in
+    let new_type_2 = EConstr.mkSort s in
+    let evd, _ =
+      Typing.type_of (Global.env()) (Evd.from_env (Global.env())) new_type_2 in
+    Feedback.msg_notice
+      (Printer.pr_econstr_env env evd new_type_2) }
+END
+
+VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
+| [ "Tuto3_2" ] -> { example_sort_app_lambda () }
+END
+
+TACTIC EXTEND collapse_hyps
+| [ "pack" "hypothesis" ident(i) ] ->
+  { Tuto_tactic.pack_tactic i }
+END
+
+(* More advanced examples, where automatic proof happens but
+   no tactic is being called explicitely.  The first one uses
+   type classes. *)
+VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
+| [ "Tuto3_3" int(n) ] -> { example_classes n }
+END
+
+(* The second one uses canonical structures. *)
+VERNAC COMMAND EXTEND TriggerCanonical CLASSIFIED AS QUERY
+| [ "Tuto3_4" int(n) ] -> { example_canonical n }
+END
+
-- 
cgit v1.2.3