Merge PR #8161: Implement VERNAC EXTEND in coqpp

4 files changed, 15 insertions, 21 deletions

diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index f3af318b60..b163100fc3 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -50,3 +50,5 @@ val type_of_user_symbol : user_symbol -> argument_type
 val parse_user_entry : string -> string -> user_symbol
 
 val mlexpr_of_symbol : user_symbol -> MLast.expr
+
+val binders_of_tokens : MLast.expr -> extend_token list -> MLast.expr
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp
index 0e2bf55d86..a2007d258c 100644
--- a/grammar/q_util.mlp
+++ b/grammar/q_util.mlp
@@ -142,3 +142,9 @@ let rec mlexpr_of_symbol = function
   assert (e = "tactic");
   let wit = <:expr< $lid:"wit_"^e$ >> in
   <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>>
+
+let rec binders_of_tokens e = function
+| [] -> e
+| ExtNonTerminal(_,None) :: cl -> <:expr< fun _ -> $binders_of_tokens e cl$ >>
+| ExtNonTerminal(_,Some id) :: cl -> <:expr< fun $lid:id$ -> $binders_of_tokens e cl$ >>
+| ExtTerminal _ :: cl -> binders_of_tokens e cl
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index 5943600b7c..a093f78388 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -20,16 +20,8 @@ let plugin_name = <:expr< __coq_plugin_name >>
 let rec mlexpr_of_clause = function
 | [] -> <:expr< TyNil >>
 | ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >>
-| ExtNonTerminal(g,None) :: cl ->
-  <:expr< TyAnonArg($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >>
-| ExtNonTerminal(g,Some id) :: cl ->
-  <:expr< TyArg($mlexpr_of_symbol g$, $mlexpr_of_string id$, $mlexpr_of_clause cl$) >>
-
-let rec binders_of_clause e = function
-| [] -> <:expr< fun ist -> $e$ >>
-| ExtNonTerminal(_,None) :: cl -> binders_of_clause e cl
-| ExtNonTerminal(_,Some id) :: cl -> <:expr< fun $lid:id$ -> $binders_of_clause e cl$ >>
-| _ :: cl -> binders_of_clause e cl
+| ExtNonTerminal (g, _) :: cl ->
+  <:expr< TyArg($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >>
 
 open Pcaml
 
@@ -52,7 +44,8 @@ EXTEND
   tacrule:
     [ [ "["; l = LIST1 tacargs; "]";
         "->"; "["; e = Pcaml.expr; "]" ->
-         <:expr< TyML($mlexpr_of_clause l$, $binders_of_clause e l$) >>
+        let e = <:expr< fun ist -> $e$ >> in
+         <:expr< TyML($mlexpr_of_clause l$, $binders_of_tokens e l$) >>
     ] ]
   ;
 
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index f30c96a7f5..3c401e827e 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -24,23 +24,16 @@ type rule = {
   (** Whether this entry is deprecated *)
 }
 
-let rec make_patt r = function
-| [] -> r
-| ExtNonTerminal (_, Some p) :: l -> <:expr< fun $lid:p$ -> $make_patt r l$ >>
-| ExtNonTerminal (_, None) :: l -> <:expr< fun _ -> $make_patt r l$ >>
-| ExtTerminal _ :: l -> make_patt r l
-
 let rec mlexpr_of_clause = function
 | [] -> <:expr< Vernacentries.TyNil >>
 | ExtTerminal s :: cl -> <:expr< Vernacentries.TyTerminal ($str:s$, $mlexpr_of_clause cl$) >>
 | ExtNonTerminal (g, id) :: cl ->
-  let id = mlexpr_of_option mlexpr_of_string id in
-  <:expr< Vernacentries.TyNonTerminal ($id$, $mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >>
+  <:expr< Vernacentries.TyNonTerminal ($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >>
 
 let make_rule r =
   let ty = mlexpr_of_clause r.r_patt in
-  let cmd = make_patt r.r_branch r.r_patt in
-  let make_classifier c = make_patt c r.r_patt in
+  let cmd = binders_of_tokens r.r_branch r.r_patt in
+  let make_classifier c = binders_of_tokens c r.r_patt in
   let classif = mlexpr_of_option make_classifier r.r_class in
   <:expr< Vernacentries.TyML ($mlexpr_of_bool r.r_depr$, $ty$, $cmd$, $classif$) >>