Merge pull request #14 from ppedrot/coqpp-port

Port to coqpp.

1 files changed, 10 insertions, 6 deletions

diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.mlg
index 71c6be16c8..82ba45726e 100644
--- a/tuto3/src/g_tuto3.ml4
+++ b/tuto3/src/g_tuto3.mlg
@@ -1,5 +1,7 @@
 DECLARE PLUGIN "tuto3_plugin"
 
+{
+
 open Ltac_plugin
 
 open Construction_game
@@ -7,36 +9,38 @@ 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 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) ]
+      (Printer.pr_econstr_env env evd new_type_2) }
 END
 
 VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
-| [ "Tuto3_2" ] -> [ example_sort_app_lambda () ]
+| [ "Tuto3_2" ] -> { example_sort_app_lambda () }
 END
 
 TACTIC EXTEND collapse_hyps
 | [ "pack" "hypothesis" ident(i) ] ->
-  [ Tuto_tactic.pack_tactic 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 ]
+| [ "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 ]
+| [ "Tuto3_4" int(n) ] -> { example_canonical n }
 END