Port to coqpp.

8 files changed, 98 insertions, 57 deletions

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.mlg
index d6e95ba0f7..5c633fe862 100644
--- a/tuto0/src/g_tuto0.ml4
+++ b/tuto0/src/g_tuto0.mlg
@@ -1,14 +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) ]
+| [ "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 ]
+  { let _ = Feedback.msg_notice (str Tuto0_main.message) in
+    Tacticals.New.tclIDTAC }
 END
diff --git a/tuto1/_CoqProject b/tuto1/_CoqProject
index ce14ee2b87..585d1360be 100644
--- a/tuto1/_CoqProject
+++ b/tuto1/_CoqProject
@@ -9,5 +9,5 @@ src/simple_declare.mli
 src/simple_declare.ml
 src/simple_print.ml
 src/simple_print.mli
-src/g_tuto1.ml4
-src/tuto1_plugin.mlpack
\ No newline at end of file
+src/g_tuto1.mlg
+src/tuto1_plugin.mlpack
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.mlg
index 1f4660d1f0..4df284d2d9 100644
--- a/tuto1/src/g_tuto1.ml4
+++ b/tuto1/src/g_tuto1.mlg
@@ -1,19 +1,24 @@
 DECLARE PLUGIN "tuto1_plugin"
 
+{
+
 (* If we forget this line and include our own tactic definition using
   TACTIC EXTEND, as below, then we get the strange error message
   no implementation available for Tacentries, only when compiling
   theories/Loader.v
 *)
 open Ltac_plugin
+open Attributes
 open Pp
 (* This module defines the types of arguments to be used in the
    EXTEND directives below, for example the string one. *)
 open Stdarg
 
+}
+
 VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
 | [ "Hello" string(s) ] ->
-  [ Feedback.msg_notice (strbrk "Hello " ++ str s) ]
+  { Feedback.msg_notice (strbrk "Hello " ++ str s) }
 END
 
 (* reference is allowed as a syntactic entry, but so are all the entries
@@ -23,8 +28,8 @@ VERNAC COMMAND EXTEND HelloAgain CLASSIFIED AS QUERY
 | [ "HelloAgain" reference(r)] ->
 (* The function Ppconstr.pr_qualid was found by searching all mli files
    for a function of type qualid -> Pp.t *)
-  [ Feedback.msg_notice
-      (strbrk "Hello again " ++ Ppconstr.pr_qualid r)]
+  { Feedback.msg_notice
+      (strbrk "Hello again " ++ Ppconstr.pr_qualid r)}
 END
 
 (* According to parsing/pcoq.mli, e has type constr_expr *)
@@ -33,7 +38,7 @@ END
    constrexpr.mli --> Easier for packing the software in components. *)
 VERNAC COMMAND EXTEND TakingConstr CLASSIFIED AS QUERY
 | [ "Cmd1" constr(e) ] ->
-  [ let _ = e in Feedback.msg_notice (strbrk "Cmd1 parsed something") ]
+  { let _ = e in Feedback.msg_notice (strbrk "Cmd1 parsed something") }
 END
 
 (* The next step is to make something of parsed expression.
@@ -45,12 +50,12 @@ END
 
 VERNAC COMMAND EXTEND TakingConstr2 CLASSIFIED AS QUERY
 | [ "Cmd2" constr(e) ] ->
-  [ let _ = Constrintern.interp_constr
+  { let _ = Constrintern.interp_constr
     (Global.env())
     (* Make sure you don't use Evd.empty here, as this does not
       check consistency with existing universe constraints. *)
     (Evd.from_env (Global.env())) e in
-    Feedback.msg_notice (strbrk "Cmd2 parsed something legitimate") ]
+    Feedback.msg_notice (strbrk "Cmd2 parsed something legitimate") }
 END
 
 (* This is to show what happens when typing in an empty environment
@@ -60,10 +65,10 @@ END
  
 VERNAC COMMAND EXTEND TakingConstr3 CLASSIFIED AS QUERY
 | [ "Cmd3" constr(e) ] ->
-  [ let _ = Constrintern.interp_constr Environ.empty_env
+  { let _ = Constrintern.interp_constr Environ.empty_env
       Evd.empty e in
       Feedback.msg_notice
-        (strbrk "Cmd3 accepted something in the empty context")]
+        (strbrk "Cmd3 accepted something in the empty context")}
 END
 
 (* When adding a definition, we have to be careful that just
@@ -78,41 +83,41 @@ END
   there was "EConstr.constr" and not "Constr.constr". *)
 
 VERNAC COMMAND EXTEND Define1 CLASSIFIED AS SIDEFF
-| [ "Cmd4" ident(i) constr(e) ] ->
-  [ let v = Constrintern.interp_constr (Global.env())
+| #[ poly = polymorphic ] [ "Cmd4" ident(i) constr(e) ] ->
+  { let v = Constrintern.interp_constr (Global.env())
       (Evd.from_env (Global.env())) e in
-    Simple_declare.packed_declare_definition ~poly:(Attributes.(parse polymorphic atts)) i v ]
+    Simple_declare.packed_declare_definition ~poly i v }
 END
 
 VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
 | [ "Cmd5" constr(e) ] ->
-  [ let v = Constrintern.interp_constr (Global.env())
+  { let v = Constrintern.interp_constr (Global.env())
       (Evd.from_env (Global.env())) e in
     let (_, ctx) = v in
     let evd = Evd.from_ctx ctx in
     Feedback.msg_notice
     (Printer.pr_econstr_env (Global.env()) evd
-       (Simple_check.simple_check1 v)) ]
+       (Simple_check.simple_check1 v)) }
 END
 
 VERNAC COMMAND EXTEND Check2 CLASSIFIED AS QUERY
 | [ "Cmd6" constr(e) ] ->
-  [ let v = Constrintern.interp_constr (Global.env())
+  { let v = Constrintern.interp_constr (Global.env())
       (Evd.from_env (Global.env())) e in
     let evd, ty = Simple_check.simple_check2 v in
     Feedback.msg_notice
-      (Printer.pr_econstr_env (Global.env()) evd ty) ]
+      (Printer.pr_econstr_env (Global.env()) evd ty) }
 END
 
 VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
 | [ "Cmd7" constr(e) ] ->
-  [ let v = Constrintern.interp_constr (Global.env())
+  { let v = Constrintern.interp_constr (Global.env())
       (Evd.from_env (Global.env())) e in
     let (a, ctx) = v in
     let evd = Evd.from_ctx ctx in
       Feedback.msg_notice
       (Printer.pr_econstr_env (Global.env()) evd
-         (Simple_check.simple_check3 v)) ]
+         (Simple_check.simple_check3 v)) }
 END
 
 (* This command takes a name and return its value.  It does less
@@ -122,17 +127,17 @@ END
   intended use. *)
 VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY
 | [ "Cmd8" reference(r) ] ->
-  [ let env = Global.env() in
+  { let env = Global.env() in
     let evd = Evd.from_env env in
     Feedback.msg_notice
     (Printer.pr_econstr_env env evd
       (EConstr.of_constr
-        (Simple_print.simple_body_access (Nametab.global r)))) ]
+        (Simple_print.simple_body_access (Nametab.global r)))) }
 END
 
 TACTIC EXTEND my_intro
 | [ "my_intro" ident(i) ] ->
-  [ Tactics.introduction i]
+  { Tactics.introduction i }
 END
 
 (* if one write this:
@@ -141,9 +146,9 @@ END
 
 VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
 | [ "Cmd9" ] ->
-  [ let p = Proof_global.give_me_the_proof () in
+  { let p = Proof_global.give_me_the_proof () in
     let sigma, env = Pfedit.get_current_context () in
     let pprf = Proof.partial_proof p in
     Feedback.msg_notice
-      (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) ]
+      (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) }
 END
diff --git a/tuto2/_CoqProject b/tuto2/_CoqProject
index bdafdb5f04..cf9cb5cc26 100644
--- a/tuto2/_CoqProject
+++ b/tuto2/_CoqProject
@@ -2,5 +2,5 @@
 -I src
 
 theories/Test.v
-src/demo.ml4
+src/demo.mlg
 src/demo_plugin.mlpack
diff --git a/tuto2/src/demo.ml4 b/tuto2/src/demo.mlg
index 981d41fa5c..966c05acdc 100644
--- a/tuto2/src/demo.ml4
+++ b/tuto2/src/demo.mlg
@@ -25,7 +25,7 @@ DECLARE PLUGIN "demo_plugin"
    (3) The file "demo_plugin.mlpack" lists the OCaml modules to be linked in
        "demo_plugin.cmxs".
 
-   (4) The file "demo_plugin.mlpack" as well as all .ml, .mli and .ml4 files
+   (4) The file "demo_plugin.mlpack" as well as all .ml, .mli and .mlg files
        are listed in the "_CoqProject" file.
 *)
 
@@ -36,7 +36,7 @@ DECLARE PLUGIN "demo_plugin"
 (* -------------------------------------------------------------------------- *)
 
 VERNAC COMMAND EXTEND Cmd1 CLASSIFIED AS QUERY
-  [ "Cmd1" ] -> [ () ]
+| [ "Cmd1" ] -> { () }
 END
 
 (*
@@ -64,7 +64,7 @@ END
 
    This:
 
-     [ "Cmd1" ] -> [ () ]
+     [ "Cmd1" ] -> { () }
 
    defines:
    - the parsing rule
@@ -84,10 +84,10 @@ END
    
    The interpretation rule, in this case, is:
 
-     [ () ]
+     { () }
 
-   Like in case of the parsing rule,
-   [ and ] characters mark the beginning and the end of the interpretation rule.
+   Similarly to the case of the parsing rule,
+   { and } characters mark the beginning and the end of the interpretation rule.
    In this case, the following Ocaml expression:
 
      ()
@@ -103,7 +103,7 @@ END
 (* -------------------------------------------------------------------------- *)
 
 VERNAC COMMAND EXTEND Cmd2 CLASSIFIED AS QUERY
-  [ "Cmd2" "With" "Some" "Terminal" "Parameters" ] -> [ () ]
+| [ "Cmd2" "With" "Some" "Terminal" "Parameters" ] -> { () }
 END
 
 (*
@@ -119,10 +119,14 @@ END
 (*                                                                            *)
 (* -------------------------------------------------------------------------- *)
 
+{
+
 open Stdarg
 
+}
+
 VERNAC COMMAND EXTEND Cmd3 CLASSIFIED AS QUERY
-  [ "Cmd3" int(i) ] -> [ () ]
+| [ "Cmd3" int(i) ] -> { () }
 END
 
 (*
@@ -179,7 +183,7 @@ END
 (* -------------------------------------------------------------------------- *)
 
 VERNAC COMMAND EXTEND Cmd4 CLASSIFIED AS QUERY
-  [ "Cmd4" int_list(l) ] -> [ () ]
+| [ "Cmd4" int_list(l) ] -> { () }
 END
 
 (*
@@ -211,8 +215,12 @@ END
 (*                                                                            *)
 (* -------------------------------------------------------------------------- *)
 
+{
+
 open Ltac_plugin
 
+}
+
 (*
    If we want to avoid a compilation failure
 
@@ -226,8 +234,12 @@ open Ltac_plugin
    do not expand to fully qualified names.
 *)
 
+{
+
 type type_5 = Foo_5 | Bar_5
 
+}
+
 (*
    We define a type of values that we want to pass to our Vernacular command.
 *)
@@ -241,11 +253,15 @@ type type_5 = Foo_5 | Bar_5
    of a type that is not supported by default, we must use the following macro:
 *)
 
+{
+
 open Pp
 
+}
+
 VERNAC ARGUMENT EXTEND custom5
-| [ "Foo_5" ] -> [ Foo_5 ]
-| [ "Bar_5" ] -> [ Bar_5 ]
+| [ "Foo_5" ] -> { Foo_5 }
+| [ "Bar_5" ] -> { Bar_5 }
 END
 
 (*
@@ -265,7 +281,7 @@ END
 (* Here: *)
 
 VERNAC COMMAND EXTEND Cmd5 CLASSIFIED AS QUERY
-  [ "Cmd5" custom5(x) ] -> [ () ]
+| [ "Cmd5" custom5(x) ] -> { () }
 END
 
 (*
@@ -280,7 +296,7 @@ END
 (* -------------------------------------------------------------------------- *)
 
 VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY
-  [ "Cmd6" ] -> [ Feedback.msg_notice (Pp.str "Everything is awesome!") ]
+| [ "Cmd6" ] -> { Feedback.msg_notice (Pp.str "Everything is awesome!") }
 END
 
 (*
@@ -306,8 +322,12 @@ END
 (*                                                                            *)
 (* -------------------------------------------------------------------------- *)
 
+{
+
 open Summary.Local
 
+}
+
 (*
    By opening Summary.Local module we shadow the original functions
    that we traditionally use for implementing stateful behavior.
@@ -318,30 +338,38 @@ open Summary.Local
 
    are now shadowed by their counterparts in Summary.Local. *)
 
+{
+
 let counter = ref ~name:"counter" 0
 
+}
+
 VERNAC COMMAND EXTEND Cmd7 CLASSIFIED AS SIDEFF
-  [ "Cmd7" ] -> [ counter := succ !counter;
-                  Feedback.msg_notice (Pp.str "counter = " ++ Pp.str (string_of_int (!counter))) ]
+| [ "Cmd7" ] -> { counter := succ !counter;
+                  Feedback.msg_notice (Pp.str "counter = " ++ Pp.str (string_of_int (!counter))) }
 END
 
 TACTIC EXTEND tactic1
-  [ "tactic1" ] -> [ Proofview.tclUNIT () ]
+| [ "tactic1" ] -> { Proofview.tclUNIT () }
 END
 
 (* ---- *)
 
+{
+
 type custom = Foo_2 | Bar_2
 
 let pr_custom _ _ _ = function
   | Foo_2 -> Pp.str "Foo_2"
   | Bar_2 -> Pp.str "Bar_2"
 
-ARGUMENT EXTEND custom2 PRINTED BY pr_custom
-| [ "Foo_2" ] -> [ Foo_2 ]
-| [ "Bar_2" ] -> [ Bar_2 ]
+}
+
+ARGUMENT EXTEND custom2 PRINTED BY { pr_custom }
+| [ "Foo_2" ] -> { Foo_2 }
+| [ "Bar_2" ] -> { Bar_2 }
 END
 
 TACTIC EXTEND tactic2
-  [ "tactic2" custom2(x) ] -> [ Proofview.tclUNIT () ]
+| [ "tactic2" custom2(x) ] -> { Proofview.tclUNIT () }
 END
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.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