Merge PR #8733: Implement ARGUMENT EXTEND in coqpp

1 files changed, 53 insertions, 34 deletions

diff --git a/plugins/ssrmatching/g_ssrmatching.ml4 b/plugins/ssrmatching/g_ssrmatching.mlg
index 746c368aa9..3f0794fdd4 100644
--- a/plugins/ssrmatching/g_ssrmatching.ml4
+++ b/plugins/ssrmatching/g_ssrmatching.mlg
@@ -8,8 +8,9 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+{
+
 open Ltac_plugin
-open Genarg
 open Pcoq
 open Pcoq.Constr
 open Ssrmatching
@@ -19,83 +20,101 @@ open Ssrmatching.Internal
  * we thus save the lexer to restore it at the end of the file *)
 let frozen_lexer = CLexer.get_keyword_state () ;;
 
+}
+
 DECLARE PLUGIN "ssrmatching_plugin"
 
+{
+
 let pr_rpattern _ _ _ = pr_rpattern
 
+}
+
 ARGUMENT EXTEND rpattern
   TYPED AS rpatternty
-  PRINTED BY pr_rpattern
-  INTERPRETED BY interp_rpattern
-  GLOBALIZED BY glob_rpattern
-  SUBSTITUTED BY subst_rpattern
-  | [ lconstr(c) ] -> [ mk_rpattern (T (mk_lterm c None)) ]
-  | [ "in" lconstr(c) ] -> [ mk_rpattern (In_T (mk_lterm c None)) ]
+  PRINTED BY { pr_rpattern }
+  INTERPRETED BY { interp_rpattern }
+  GLOBALIZED BY { glob_rpattern }
+  SUBSTITUTED BY { subst_rpattern }
+  | [ lconstr(c) ] -> { mk_rpattern (T (mk_lterm c None)) }
+  | [ "in" lconstr(c) ] -> { mk_rpattern (In_T (mk_lterm c None)) }
   | [ lconstr(x) "in" lconstr(c) ] ->
-    [ mk_rpattern (X_In_T (mk_lterm x None, mk_lterm c None)) ]
+    { mk_rpattern (X_In_T (mk_lterm x None, mk_lterm c None)) }
   | [ "in" lconstr(x) "in" lconstr(c) ] ->
-    [ mk_rpattern (In_X_In_T (mk_lterm x None, mk_lterm c None)) ]
+    { mk_rpattern (In_X_In_T (mk_lterm x None, mk_lterm c None)) }
   | [ lconstr(e) "in" lconstr(x) "in" lconstr(c) ] ->
-    [ mk_rpattern (E_In_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None)) ]
+    { mk_rpattern (E_In_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None)) }
   | [ lconstr(e) "as" lconstr(x) "in" lconstr(c) ] ->
-    [ mk_rpattern (E_As_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None)) ]
+    { mk_rpattern (E_As_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None)) }
 END
 
+{
+
 let pr_ssrterm _ _ _ = pr_ssrterm
 
+}
+
 ARGUMENT EXTEND cpattern
-     PRINTED BY pr_ssrterm
-     INTERPRETED BY interp_ssrterm
-     GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm
-     RAW_PRINTED BY pr_ssrterm
-     GLOB_PRINTED BY pr_ssrterm
-| [ "Qed" constr(c) ] -> [ mk_lterm c None ]
+     PRINTED BY { pr_ssrterm }
+     INTERPRETED BY { interp_ssrterm }
+     GLOBALIZED BY { glob_cpattern } SUBSTITUTED BY { subst_ssrterm }
+     RAW_PRINTED BY { pr_ssrterm }
+     GLOB_PRINTED BY { pr_ssrterm }
+| [ "Qed" constr(c) ] -> { mk_lterm c None }
 END
 
+{
+
 let input_ssrtermkind strm = match Util.stream_nth 0 strm with
   | Tok.KEYWORD "(" -> '('
   | Tok.KEYWORD "@" -> '@'
   | _ -> ' '
 let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
 
-GEXTEND Gram
+}
+
+GRAMMAR EXTEND Gram
   GLOBAL: cpattern;
-  cpattern: [[ k = ssrtermkind; c = constr ->
+  cpattern: [[ k = ssrtermkind; c = constr -> {
     let pattern = mk_term k c None in
-    if loc_of_cpattern pattern <> Some !@loc && k = '('
+    if loc_of_cpattern pattern <> Some loc && k = '('
     then mk_term 'x' c None
-    else pattern ]];
+    else pattern } ]];
 END
 
 ARGUMENT EXTEND lcpattern
      TYPED AS cpattern
-     PRINTED BY pr_ssrterm
-     INTERPRETED BY interp_ssrterm
-     GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm
-     RAW_PRINTED BY pr_ssrterm
-     GLOB_PRINTED BY pr_ssrterm
-| [ "Qed" lconstr(c) ] -> [ mk_lterm c None ]
+     PRINTED BY { pr_ssrterm }
+     INTERPRETED BY { interp_ssrterm }
+     GLOBALIZED BY { glob_cpattern } SUBSTITUTED BY { subst_ssrterm }
+     RAW_PRINTED BY { pr_ssrterm }
+     GLOB_PRINTED BY { pr_ssrterm }
+| [ "Qed" lconstr(c) ] -> { mk_lterm c None }
 END
 
-GEXTEND Gram
+GRAMMAR EXTEND Gram
   GLOBAL: lcpattern;
-  lcpattern: [[ k = ssrtermkind; c = lconstr ->
+  lcpattern: [[ k = ssrtermkind; c = lconstr -> {
     let pattern = mk_term k c None in
-    if loc_of_cpattern pattern <> Some !@loc && k = '('
+    if loc_of_cpattern pattern <> Some loc && k = '('
     then mk_term 'x' c None
-    else pattern ]];
+    else pattern } ]];
 END
 
-ARGUMENT EXTEND ssrpatternarg TYPED AS rpattern PRINTED BY pr_rpattern
-| [ rpattern(pat) ] -> [ pat ]
+ARGUMENT EXTEND ssrpatternarg TYPED AS rpattern PRINTED BY { pr_rpattern }
+| [ rpattern(pat) ] -> { pat }
 END
 
 TACTIC EXTEND ssrinstoftpat
-| [ "ssrinstancesoftpat" cpattern(arg) ] -> [ Proofview.V82.tactic (ssrinstancesof arg) ]
+| [ "ssrinstancesoftpat" cpattern(arg) ] -> { Proofview.V82.tactic (ssrinstancesof arg) }
 END
 
+{
+
 (* We wipe out all the keywords generated by the grammar rules we defined. *)
 (* The user is supposed to Require Import ssreflect or Require ssreflect   *)
 (* and Import ssreflect.SsrSyntax to obtain these keywords and as a         *)
 (* consequence the extended ssreflect grammar.                             *)
 let () = CLexer.set_keyword_state frozen_lexer ;;
+
+}