Merge PR #8733: Implement ARGUMENT EXTEND in coqpp

1 files changed, 51 insertions, 31 deletions

diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.mlg
index 4ea0b30bd7..3ddea7eb30 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.mlg
@@ -8,6 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+{
+
 open Ltac_plugin
 open Pp
 open Util
@@ -20,15 +22,19 @@ open Tacarg
 open Pcoq.Constr
 open Pltac
 
+}
+
 DECLARE PLUGIN "newring_plugin"
 
 TACTIC EXTEND protect_fv
-  [ "protect_fv" string(map) "in" ident(id) ] ->
-    [ protect_tac_in map id ]
+| [ "protect_fv" string(map) "in" ident(id) ] ->
+    { protect_tac_in map id }
 | [ "protect_fv" string(map) ] ->
-    [ protect_tac map ]
+    { protect_tac map }
 END
 
+{
+
 open Pptactic
 open Ppconstr
 
@@ -46,35 +52,41 @@ let pr_ring_mod = function
   | Sign_spec t -> str "sign" ++ pr_arg pr_constr_expr t
   | Div_spec t -> str "div" ++ pr_arg pr_constr_expr t
 
+}
+
 VERNAC ARGUMENT EXTEND ring_mod
-  PRINTED BY pr_ring_mod
-  | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ]
-  | [ "abstract" ] -> [ Ring_kind Abstract ]
-  | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ]
-  | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ]
-  | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ]
-  | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ]
-  | [ "postprocess" "[" tactic(post) "]" ] -> [ Post_tac post ]
-  | [ "setoid" constr(sth) constr(ext) ] -> [ Setoid(sth,ext) ]
-  | [ "sign" constr(sign_spec) ] -> [ Sign_spec sign_spec ]
+  PRINTED BY { pr_ring_mod }
+  | [ "decidable" constr(eq_test) ] -> { Ring_kind(Computational eq_test) }
+  | [ "abstract" ] -> { Ring_kind Abstract }
+  | [ "morphism" constr(morph) ] -> { Ring_kind(Morphism morph) }
+  | [ "constants" "[" tactic(cst_tac) "]" ] -> { Const_tac(CstTac cst_tac) }
+  | [ "closed" "[" ne_global_list(l) "]" ] -> { Const_tac(Closed l) }
+  | [ "preprocess" "[" tactic(pre) "]" ] -> { Pre_tac pre }
+  | [ "postprocess" "[" tactic(post) "]" ] -> { Post_tac post }
+  | [ "setoid" constr(sth) constr(ext) ] -> { Setoid(sth,ext) }
+  | [ "sign" constr(sign_spec) ] -> { Sign_spec sign_spec }
   | [ "power" constr(pow_spec) "[" ne_global_list(l) "]" ] ->
-           [ Pow_spec (Closed l, pow_spec) ]
+           { Pow_spec (Closed l, pow_spec) }
   | [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] ->
-           [ Pow_spec (CstTac cst_tac, pow_spec) ]
-  | [ "div" constr(div_spec) ] -> [ Div_spec div_spec ]
+           { Pow_spec (CstTac cst_tac, pow_spec) }
+  | [ "div" constr(div_spec) ] -> { Div_spec div_spec }
 END
 
+{
+
 let pr_ring_mods l = surround (prlist_with_sep pr_comma pr_ring_mod l)
 
+}
+
 VERNAC ARGUMENT EXTEND ring_mods
-  PRINTED BY pr_ring_mods
-  | [ "(" ne_ring_mod_list_sep(mods, ",") ")" ] -> [ mods ]
+  PRINTED BY { pr_ring_mods }
+  | [ "(" ne_ring_mod_list_sep(mods, ",") ")" ] -> { mods }
 END
 
 VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
   | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods_opt(l) ] ->
-    [ let l = match l with None -> [] | Some l -> l in add_theory id t l]
-  | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [
+    { let l = match l with None -> [] | Some l -> l in add_theory id t l }
+  | [ "Print" "Rings" ] => {Vernac_classifier.classify_as_query} -> {
     Feedback.msg_notice (strbrk "The following ring structures have been declared:");
     Spmap.iter (fun fn fi ->
       let sigma, env = Pfedit.get_current_context () in
@@ -82,35 +94,43 @@ VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
         (Ppconstr.pr_id (Libnames.basename fn)++spc()++
           str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++
           str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req))
-    ) !from_name ]
+    ) !from_name }
 END
 
 TACTIC EXTEND ring_lookup
 | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] ->
-    [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t ]
+    { let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t }
 END
 
+{
+
 let pr_field_mod = function
   | Ring_mod m -> pr_ring_mod m
   | Inject inj -> str "completeness" ++ pr_arg pr_constr_expr inj
 
+}
+
 VERNAC ARGUMENT EXTEND field_mod
-  PRINTED BY pr_field_mod
-  | [ ring_mod(m) ] -> [ Ring_mod m ]
-  | [ "completeness" constr(inj) ] -> [ Inject inj ]
+  PRINTED BY { pr_field_mod }
+  | [ ring_mod(m) ] -> { Ring_mod m }
+  | [ "completeness" constr(inj) ] -> { Inject inj }
 END
 
+{
+
 let pr_field_mods l = surround (prlist_with_sep pr_comma pr_field_mod l)
 
+}
+
 VERNAC ARGUMENT EXTEND field_mods
-  PRINTED BY pr_field_mods
-  | [ "(" ne_field_mod_list_sep(mods, ",") ")" ] -> [ mods ]
+  PRINTED BY { pr_field_mods }
+  | [ "(" ne_field_mod_list_sep(mods, ",") ")" ] -> { mods }
 END
 
 VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
 | [ "Add" "Field" ident(id) ":" constr(t) field_mods_opt(l) ] ->
-  [ let l = match l with None -> [] | Some l -> l in add_field_theory id t l ]
-| [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [
+  { let l = match l with None -> [] | Some l -> l in add_field_theory id t l }
+| [ "Print" "Fields" ] => {Vernac_classifier.classify_as_query} -> {
     Feedback.msg_notice (strbrk "The following field structures have been declared:");
     Spmap.iter (fun fn fi ->
       let sigma, env = Pfedit.get_current_context () in
@@ -118,10 +138,10 @@ VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
         (Ppconstr.pr_id (Libnames.basename fn)++spc()++
           str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++
           str"and equivalence relation "++ pr_constr_env env sigma fi.field_req))
-    ) !field_from_name ]
+    ) !field_from_name }
 END
 
 TACTIC EXTEND field_lookup
 | [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] ->
-      [ let (t,l) = List.sep_last lt in field_lookup f lH l t ]
+      { let (t,l) = List.sep_last lt in field_lookup f lH l t }
 END