Rename tac2type -> ltac2_type,

typ_param -> ltac2_typevar,
tac2expr -> ltac2_expr

6 files changed, 137 insertions, 139 deletions

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index d75b5f6965..754e73badf 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -207,19 +207,19 @@ tactic_then_last: [
 ]
 
 ltac2_tactic_then_last: [
-| REPLACE "|" LIST0 ( OPT tac2expr6 ) SEP "|"      (* Ltac2 plugin *)
-| WITH LIST0 (  "|" OPT tac2expr6 )  TAG Ltac2
+| REPLACE "|" LIST0 ( OPT ltac2_expr6 ) SEP "|"      (* Ltac2 plugin *)
+| WITH LIST0 (  "|" OPT ltac2_expr6 )  TAG Ltac2
 ]
 
 ltac2_goal_tactics: [
-| LIST0 ( OPT tac2expr6 ) SEP "|"  TAG Ltac2
+| LIST0 ( OPT ltac2_expr6 ) SEP "|"  TAG Ltac2
 ]
 
 ltac2_for_each_goal: [ | DELETENT ]
 
 ltac2_for_each_goal: [
 | ltac2_goal_tactics  TAG Ltac2
-| OPT ( ltac2_goal_tactics "|" ) OPT tac2expr6 ".." OPT ( "|" ltac2_goal_tactics )  TAG Ltac2
+| OPT ( ltac2_goal_tactics "|" ) OPT ltac2_expr6 ".." OPT ( "|" ltac2_goal_tactics )  TAG Ltac2
 ]
 
 ltac2_tactic_then_last: [
@@ -1627,7 +1627,7 @@ ltac2_rewriter: [
 | OPT natural OPT [ "?" | "!" ] ltac2_constr_with_bindings
 ]
 
-tac2expr0: [
+ltac2_expr0: [
 | DELETE "(" ")"
 ]
 
@@ -1961,7 +1961,7 @@ ltac2_match_key: [
 ]
 
 ltac2_constructs: [
-| ltac2_match_key tac2expr6 "with" ltac2_match_list "end"
+| ltac2_match_key ltac2_expr6 "with" ltac2_match_list "end"
 | ltac2_match_key OPT "reverse" "goal" "with" goal_match_list "end"
 ]
 
@@ -2058,7 +2058,7 @@ atomic_tac2pat: [
 | OPTINREF
 ]
 
-tac2expr0: [
+ltac2_expr0: [
 (*
 | DELETE "(" ")" (* covered by "()" prodn *)
 | REPLACE "{" [  | LIST1 tac2rec_fieldexpr OPT ";" ] "}"
@@ -2071,13 +2071,13 @@ tac2expr0: [
 use LIST1? *)
 
 SPLICE: [
-| tac2expr4
+| ltac2_expr4
 ]
 
-tac2expr3: [
-| REPLACE tac2expr2 "," LIST1 tac2expr2 SEP ","      (* Ltac2 plugin *)
-| WITH LIST1 tac2expr2 SEP "," TAG Ltac2
-| DELETE tac2expr2      (* Ltac2 plugin *)
+ltac2_expr3: [
+| REPLACE ltac2_expr2 "," LIST1 ltac2_expr2 SEP ","      (* Ltac2 plugin *)
+| WITH LIST1 ltac2_expr2 SEP "," TAG Ltac2
+| DELETE ltac2_expr2      (* Ltac2 plugin *)
 ]
 
 tac2rec_fieldexprs: [
@@ -2158,7 +2158,7 @@ ltac2_entry: [
 | WITH "Ltac2" tac2def_val
 | REPLACE tac2def_ext     (* Ltac2 plugin *)
 | WITH "Ltac2" tac2def_ext
-| "Ltac2" "Notation" [ string | lident ] ":=" tac2expr6 TAG Ltac2  (* variant *)
+| "Ltac2" "Notation" [ string | lident ] ":=" ltac2_expr6 TAG Ltac2  (* variant *)
 | MOVEALLBUT command
 (* todo: MOVEALLBUT should ignore tag on "but" prodns *)
 ]
@@ -2194,10 +2194,10 @@ SPLICE: [
 | anti
 ]
 
-tac2expr5: [
-| REPLACE "let" OPT "rec" LIST1 ltac2_let_clause SEP "with" "in" tac2expr6      (* Ltac2 plugin *)
-| WITH "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" tac2expr6 TAG Ltac2
-| MOVETO simple_tactic "match" tac2expr5 "with" OPT ltac2_branches "end"      (* Ltac2 plugin *)
+ltac2_expr5: [
+| REPLACE "let" OPT "rec" LIST1 ltac2_let_clause SEP "with" "in" ltac2_expr6      (* Ltac2 plugin *)
+| WITH "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" ltac2_expr6 TAG Ltac2
+| MOVETO simple_tactic "match" ltac2_expr5 "with" OPT ltac2_branches "end"      (* Ltac2 plugin *)
 | DELETE simple_tactic
 ]
 
@@ -2270,6 +2270,10 @@ subprf: [
 | "{" (* should be removed.  See https://github.com/coq/coq/issues/12004 *)
 ]
 
+ltac2_expr: [
+| DELETE _ltac2_expr
+]
+
 SPLICE: [
 | clause
 | noedit_mode
@@ -2450,7 +2454,6 @@ SPLICE: [
 | refglobals (* Ltac2 *)
 | syntax_modifiers
 | array_elems
-| ltac2_expr
 | G_LTAC2_input_fun
 | ltac2_simple_intropattern_closed
 | ltac2_with_bindings
@@ -2487,17 +2490,8 @@ RENAME: [
 | searchabout_query search_item
 *)
 | Pltac.tactic ltac_expr  (* many uses in EXTENDs *)
-| tac2type5 ltac2_type (* careful *)
-| tac2type2 ltac2_type2
-| tac2type1 ltac2_type1
-| tac2type0 ltac2_type0
-| typ_param ltac2_typevar
-| tac2expr6 ltac2_expr
-| tac2expr5 ltac2_expr5
-| tac2expr3 ltac2_expr3
-| tac2expr2 ltac2_expr2
-| tac2expr1 ltac2_expr1
-| tac2expr0 ltac2_expr0
+| ltac2_type5 ltac2_type
+| ltac2_expr6 ltac2_expr
 | starredidentref starred_ident_ref
 ]
 
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index a8cade6041..97d670522d 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -690,7 +690,7 @@ command: [
 | "Numeral" "Notation" reference reference reference ":" ident numeral_modifier
 | "String" "Notation" reference reference reference ":" ident
 | "Ltac2" ltac2_entry      (* Ltac2 plugin *)
-| "Ltac2" "Eval" ltac2_expr      (* Ltac2 plugin *)
+| "Ltac2" "Eval" ltac2_expr6      (* Ltac2 plugin *)
 | "Print" "Ltac2" reference      (* Ltac2 plugin *)
 ]
 
@@ -2572,50 +2572,50 @@ tac2pat0: [
 
 atomic_tac2pat: [
 |      (* Ltac2 plugin *)
-| tac2pat1 ":" tac2type5      (* Ltac2 plugin *)
+| tac2pat1 ":" ltac2_type5      (* Ltac2 plugin *)
 | tac2pat1 "," LIST0 tac2pat1 SEP ","      (* Ltac2 plugin *)
 | tac2pat1      (* Ltac2 plugin *)
 ]
 
-tac2expr6: [
-| tac2expr5 ";" tac2expr6      (* Ltac2 plugin *)
-| tac2expr5      (* Ltac2 plugin *)
+ltac2_expr6: [
+| ltac2_expr5 ";" ltac2_expr6      (* Ltac2 plugin *)
+| ltac2_expr5      (* Ltac2 plugin *)
 ]
 
-tac2expr5: [
-| "fun" LIST1 G_LTAC2_input_fun "=>" tac2expr6      (* Ltac2 plugin *)
-| "let" rec_flag LIST1 G_LTAC2_let_clause SEP "with" "in" tac2expr6      (* Ltac2 plugin *)
-| "match" tac2expr5 "with" G_LTAC2_branches "end"      (* Ltac2 plugin *)
-| tac2expr4      (* Ltac2 plugin *)
+ltac2_expr5: [
+| "fun" LIST1 G_LTAC2_input_fun "=>" ltac2_expr6      (* Ltac2 plugin *)
+| "let" rec_flag LIST1 G_LTAC2_let_clause SEP "with" "in" ltac2_expr6      (* Ltac2 plugin *)
+| "match" ltac2_expr5 "with" G_LTAC2_branches "end"      (* Ltac2 plugin *)
+| ltac2_expr4      (* Ltac2 plugin *)
 ]
 
-tac2expr4: [
-| tac2expr3      (* Ltac2 plugin *)
+ltac2_expr4: [
+| ltac2_expr3      (* Ltac2 plugin *)
 ]
 
-tac2expr3: [
-| tac2expr2 "," LIST1 tac2expr2 SEP ","      (* Ltac2 plugin *)
-| tac2expr2      (* Ltac2 plugin *)
+ltac2_expr3: [
+| ltac2_expr2 "," LIST1 ltac2_expr2 SEP ","      (* Ltac2 plugin *)
+| ltac2_expr2      (* Ltac2 plugin *)
 ]
 
-tac2expr2: [
-| tac2expr1 "::" tac2expr2      (* Ltac2 plugin *)
-| tac2expr1      (* Ltac2 plugin *)
+ltac2_expr2: [
+| ltac2_expr1 "::" ltac2_expr2      (* Ltac2 plugin *)
+| ltac2_expr1      (* Ltac2 plugin *)
 ]
 
-tac2expr1: [
-| tac2expr0 LIST1 tac2expr0      (* Ltac2 plugin *)
-| tac2expr0 ".(" Prim.qualid ")"      (* Ltac2 plugin *)
-| tac2expr0 ".(" Prim.qualid ")" ":=" tac2expr5      (* Ltac2 plugin *)
-| tac2expr0      (* Ltac2 plugin *)
+ltac2_expr1: [
+| ltac2_expr0 LIST1 ltac2_expr0      (* Ltac2 plugin *)
+| ltac2_expr0 ".(" Prim.qualid ")"      (* Ltac2 plugin *)
+| ltac2_expr0 ".(" Prim.qualid ")" ":=" ltac2_expr5      (* Ltac2 plugin *)
+| ltac2_expr0      (* Ltac2 plugin *)
 ]
 
-tac2expr0: [
-| "(" tac2expr6 ")"      (* Ltac2 plugin *)
-| "(" tac2expr6 ":" tac2type5 ")"      (* Ltac2 plugin *)
+ltac2_expr0: [
+| "(" ltac2_expr6 ")"      (* Ltac2 plugin *)
+| "(" ltac2_expr6 ":" ltac2_type5 ")"      (* Ltac2 plugin *)
 | "()"      (* Ltac2 plugin *)
 | "(" ")"      (* Ltac2 plugin *)
-| "[" LIST0 tac2expr5 SEP ";" "]"      (* Ltac2 plugin *)
+| "[" LIST0 ltac2_expr5 SEP ";" "]"      (* Ltac2 plugin *)
 | "{" tac2rec_fieldexprs "}"      (* Ltac2 plugin *)
 | G_LTAC2_tactic_atom      (* Ltac2 plugin *)
 ]
@@ -2627,7 +2627,7 @@ G_LTAC2_branches: [
 ]
 
 branch: [
-| tac2pat1 "=>" tac2expr6      (* Ltac2 plugin *)
+| tac2pat1 "=>" ltac2_expr6      (* Ltac2 plugin *)
 ]
 
 rec_flag: [
@@ -2640,7 +2640,7 @@ mut_flag: [
 |      (* Ltac2 plugin *)
 ]
 
-typ_param: [
+ltac2_typevar: [
 | "'" Prim.ident      (* Ltac2 plugin *)
 ]
 
@@ -2666,36 +2666,36 @@ ltac1_expr_in_env: [
 ]
 
 tac2expr_in_env: [
-| test_ltac1_env LIST0 locident "|-" tac2expr6      (* Ltac2 plugin *)
-| tac2expr6      (* Ltac2 plugin *)
+| test_ltac1_env LIST0 locident "|-" ltac2_expr6      (* Ltac2 plugin *)
+| ltac2_expr6      (* Ltac2 plugin *)
 ]
 
 G_LTAC2_let_clause: [
-| let_binder ":=" tac2expr6      (* Ltac2 plugin *)
+| let_binder ":=" ltac2_expr6      (* Ltac2 plugin *)
 ]
 
 let_binder: [
 | LIST1 G_LTAC2_input_fun      (* Ltac2 plugin *)
 ]
 
-tac2type5: [
-| tac2type2 "->" tac2type5      (* Ltac2 plugin *)
-| tac2type2      (* Ltac2 plugin *)
+ltac2_type5: [
+| ltac2_type2 "->" ltac2_type5      (* Ltac2 plugin *)
+| ltac2_type2      (* Ltac2 plugin *)
 ]
 
-tac2type2: [
-| tac2type1 "*" LIST1 tac2type1 SEP "*"      (* Ltac2 plugin *)
-| tac2type1      (* Ltac2 plugin *)
+ltac2_type2: [
+| ltac2_type1 "*" LIST1 ltac2_type1 SEP "*"      (* Ltac2 plugin *)
+| ltac2_type1      (* Ltac2 plugin *)
 ]
 
-tac2type1: [
-| tac2type0 Prim.qualid      (* Ltac2 plugin *)
-| tac2type0      (* Ltac2 plugin *)
+ltac2_type1: [
+| ltac2_type0 Prim.qualid      (* Ltac2 plugin *)
+| ltac2_type0      (* Ltac2 plugin *)
 ]
 
-tac2type0: [
-| "(" LIST1 tac2type5 SEP "," ")" OPT Prim.qualid      (* Ltac2 plugin *)
-| typ_param      (* Ltac2 plugin *)
+ltac2_type0: [
+| "(" LIST1 ltac2_type5 SEP "," ")" OPT Prim.qualid      (* Ltac2 plugin *)
+| ltac2_typevar      (* Ltac2 plugin *)
 | "_"      (* Ltac2 plugin *)
 | Prim.qualid      (* Ltac2 plugin *)
 ]
@@ -2714,7 +2714,7 @@ G_LTAC2_input_fun: [
 ]
 
 tac2def_body: [
-| G_LTAC2_binder LIST0 G_LTAC2_input_fun ":=" tac2expr6      (* Ltac2 plugin *)
+| G_LTAC2_binder LIST0 G_LTAC2_input_fun ":=" ltac2_expr6      (* Ltac2 plugin *)
 ]
 
 tac2def_val: [
@@ -2722,11 +2722,11 @@ tac2def_val: [
 ]
 
 tac2def_mut: [
-| "Set" Prim.qualid OPT [ "as" locident ] ":=" tac2expr6      (* Ltac2 plugin *)
+| "Set" Prim.qualid OPT [ "as" locident ] ":=" ltac2_expr6      (* Ltac2 plugin *)
 ]
 
 tac2typ_knd: [
-| tac2type5      (* Ltac2 plugin *)
+| ltac2_type5      (* Ltac2 plugin *)
 | "[" ".." "]"      (* Ltac2 plugin *)
 | "[" tac2alg_constructors "]"      (* Ltac2 plugin *)
 | "{" tac2rec_fields "}"      (* Ltac2 plugin *)
@@ -2739,7 +2739,7 @@ tac2alg_constructors: [
 
 tac2alg_constructor: [
 | Prim.ident      (* Ltac2 plugin *)
-| Prim.ident "(" LIST0 tac2type5 SEP "," ")"      (* Ltac2 plugin *)
+| Prim.ident "(" LIST0 ltac2_type5 SEP "," ")"      (* Ltac2 plugin *)
 ]
 
 tac2rec_fields: [
@@ -2750,7 +2750,7 @@ tac2rec_fields: [
 ]
 
 tac2rec_field: [
-| mut_flag Prim.ident ":" tac2type5      (* Ltac2 plugin *)
+| mut_flag Prim.ident ":" ltac2_type5      (* Ltac2 plugin *)
 ]
 
 tac2rec_fieldexprs: [
@@ -2761,13 +2761,13 @@ tac2rec_fieldexprs: [
 ]
 
 tac2rec_fieldexpr: [
-| Prim.qualid ":=" tac2expr1      (* Ltac2 plugin *)
+| Prim.qualid ":=" ltac2_expr1      (* Ltac2 plugin *)
 ]
 
 tac2typ_prm: [
 |      (* Ltac2 plugin *)
-| typ_param      (* Ltac2 plugin *)
-| "(" LIST1 typ_param SEP "," ")"      (* Ltac2 plugin *)
+| ltac2_typevar      (* Ltac2 plugin *)
+| "(" LIST1 ltac2_typevar SEP "," ")"      (* Ltac2 plugin *)
 ]
 
 tac2typ_def: [
@@ -2785,7 +2785,7 @@ tac2def_typ: [
 ]
 
 tac2def_ext: [
-| "@" "external" locident ":" tac2type5 ":=" Prim.string Prim.string      (* Ltac2 plugin *)
+| "@" "external" locident ":" ltac2_type5 ":=" Prim.string Prim.string      (* Ltac2 plugin *)
 ]
 
 syn_node: [
@@ -2806,7 +2806,7 @@ syn_level: [
 ]
 
 tac2def_syn: [
-| "Notation" LIST1 ltac2_scope syn_level ":=" tac2expr6      (* Ltac2 plugin *)
+| "Notation" LIST1 ltac2_scope syn_level ":=" ltac2_expr6      (* Ltac2 plugin *)
 ]
 
 lident: [
@@ -3024,15 +3024,15 @@ q_rewriting: [
 ]
 
 G_LTAC2_tactic_then_last: [
-| "|" LIST0 ( OPT tac2expr6 ) SEP "|"      (* Ltac2 plugin *)
+| "|" LIST0 ( OPT ltac2_expr6 ) SEP "|"      (* Ltac2 plugin *)
 |      (* Ltac2 plugin *)
 ]
 
 G_LTAC2_for_each_goal: [
-| tac2expr6 "|" G_LTAC2_for_each_goal      (* Ltac2 plugin *)
-| tac2expr6 ".." G_LTAC2_tactic_then_last      (* Ltac2 plugin *)
+| ltac2_expr6 "|" G_LTAC2_for_each_goal      (* Ltac2 plugin *)
+| ltac2_expr6 ".." G_LTAC2_tactic_then_last      (* Ltac2 plugin *)
 | ".." G_LTAC2_tactic_then_last      (* Ltac2 plugin *)
-| tac2expr6      (* Ltac2 plugin *)
+| ltac2_expr6      (* Ltac2 plugin *)
 | "|" G_LTAC2_for_each_goal      (* Ltac2 plugin *)
 |      (* Ltac2 plugin *)
 ]
@@ -3099,7 +3099,7 @@ G_LTAC2_match_pattern: [
 ]
 
 G_LTAC2_match_rule: [
-| G_LTAC2_match_pattern "=>" tac2expr6      (* Ltac2 plugin *)
+| G_LTAC2_match_pattern "=>" ltac2_expr6      (* Ltac2 plugin *)
 ]
 
 G_LTAC2_match_list: [
@@ -3120,7 +3120,7 @@ gmatch_pattern: [
 ]
 
 gmatch_rule: [
-| gmatch_pattern "=>" tac2expr6      (* Ltac2 plugin *)
+| gmatch_pattern "=>" ltac2_expr6      (* Ltac2 plugin *)
 ]
 
 goal_match_list: [
@@ -3163,7 +3163,7 @@ G_LTAC2_as_ipat: [
 ]
 
 G_LTAC2_by_tactic: [
-| "by" tac2expr6      (* Ltac2 plugin *)
+| "by" ltac2_expr6      (* Ltac2 plugin *)
 |      (* Ltac2 plugin *)
 ]
 
@@ -3186,11 +3186,11 @@ ltac2_entry: [
 ]
 
 ltac2_expr: [
-| tac2expr6      (* Ltac2 plugin *)
+| _ltac2_expr      (* Ltac2 plugin *)
 ]
 
 tac2mode: [
-| ltac2_expr ltac_use_default      (* Ltac2 plugin *)
+| ltac2_expr6 ltac_use_default      (* Ltac2 plugin *)
 | G_vernac.query_command      (* Ltac2 plugin *)
 ]
 
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 024722cf1e..6749169e8c 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -71,8 +71,9 @@ let test_ltac1_env =
     lk_ident_list >> lk_kw "|-"
   end
 
-let tac2expr = Tac2entries.Pltac.tac2expr
-let tac2type = Entry.create "tac2type"
+let ltac2_expr = Tac2entries.Pltac.ltac2_expr
+let _ltac2_expr = ltac2_expr
+let ltac2_type = Entry.create "ltac2_type"
 let tac2def_val = Entry.create "tac2def_val"
 let tac2def_typ = Entry.create "tac2def_typ"
 let tac2def_ext = Entry.create "tac2def_ext"
@@ -101,7 +102,7 @@ let pattern_of_qualid qid =
 }
 
 GRAMMAR EXTEND Gram
-  GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn
+  GLOBAL: ltac2_expr ltac2_type tac2def_val tac2def_typ tac2def_ext tac2def_syn
           tac2def_mut tac2expr_in_env;
   tac2pat:
     [ "1" LEFTA
@@ -125,7 +126,7 @@ GRAMMAR EXTEND Gram
   atomic_tac2pat:
     [ [ ->
         { CAst.make ~loc @@ CPatRef (AbsKn (Tuple 0), []) }
-      | p = tac2pat; ":"; t = tac2type ->
+      | p = tac2pat; ":"; t = ltac2_type ->
         { CAst.make ~loc @@ CPatCnv (p, t) }
       | p = tac2pat; ","; pl = LIST0 tac2pat SEP "," ->
         { let pl = p :: pl in
@@ -133,17 +134,17 @@ GRAMMAR EXTEND Gram
       | p = tac2pat -> { p }
     ] ]
   ;
-  tac2expr:
+  ltac2_expr:
     [ "6" RIGHTA
         [ e1 = SELF; ";"; e2 = SELF -> { CAst.make ~loc @@ CTacSeq (e1, e2) } ]
     | "5"
-      [ "fun"; it = LIST1 input_fun ; "=>"; body = tac2expr LEVEL "6" ->
+      [ "fun"; it = LIST1 input_fun ; "=>"; body = ltac2_expr LEVEL "6" ->
         { CAst.make ~loc @@ CTacFun (it, body) }
       | "let"; isrec = rec_flag;
           lc = LIST1 let_clause SEP "with"; "in";
-          e = tac2expr LEVEL "6" ->
+          e = ltac2_expr LEVEL "6" ->
         { CAst.make ~loc @@ CTacLet (isrec, lc, e) }
-      | "match"; e = tac2expr LEVEL "5"; "with"; bl = branches; "end" ->
+      | "match"; e = ltac2_expr LEVEL "5"; "with"; bl = branches; "end" ->
         { CAst.make ~loc @@ CTacCse (e, bl) }
       ]
     | "4" LEFTA [ ]
@@ -151,25 +152,25 @@ GRAMMAR EXTEND Gram
         { let el = e0 :: el in
           CAst.make ~loc @@ CTacApp (CAst.make ~loc @@ CTacCst (AbsKn (Tuple (List.length el))), el) } ]
     | "2" RIGHTA
-      [ e1 = tac2expr; "::"; e2 = tac2expr ->
+      [ e1 = ltac2_expr; "::"; e2 = ltac2_expr ->
         { CAst.make ~loc @@ CTacApp (CAst.make ~loc @@ CTacCst (AbsKn (Other Tac2core.Core.c_cons)), [e1; e2]) }
       ]
     | "1" LEFTA
-      [ e = tac2expr; el = LIST1 tac2expr LEVEL "0" ->
+      [ e = ltac2_expr; el = LIST1 ltac2_expr LEVEL "0" ->
         { CAst.make ~loc @@ CTacApp (e, el) }
       | e = SELF; ".("; qid = Prim.qualid; ")" ->
         { CAst.make ~loc @@ CTacPrj (e, RelId qid) }
-      | e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = tac2expr LEVEL "5" ->
+      | e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = ltac2_expr LEVEL "5" ->
         { CAst.make ~loc @@ CTacSet (e, RelId qid, r) } ]
     | "0"
       [ "("; a = SELF; ")" -> { a }
-      | "("; a = SELF; ":"; t = tac2type; ")" ->
+      | "("; a = SELF; ":"; t = ltac2_type; ")" ->
         { CAst.make ~loc @@ CTacCnv (a, t) }
       | "()" ->
         { CAst.make ~loc @@ CTacCst (AbsKn (Tuple 0)) }
       | "("; ")" ->
         { CAst.make ~loc @@ CTacCst (AbsKn (Tuple 0)) }
-      | "["; a = LIST0 tac2expr LEVEL "5" SEP ";"; "]" ->
+      | "["; a = LIST0 ltac2_expr LEVEL "5" SEP ";"; "]" ->
         { Tac2quote.of_list ~loc (fun x -> x) a }
       | "{"; a = tac2rec_fieldexprs; "}" ->
         { CAst.make ~loc @@ CTacRec a }
@@ -183,7 +184,7 @@ GRAMMAR EXTEND Gram
   ]
   ;
   branch:
-  [ [ pat = tac2pat LEVEL "1"; "=>"; e = tac2expr LEVEL "6" -> { (pat, e) } ] ]
+  [ [ pat = tac2pat LEVEL "1"; "=>"; e = ltac2_expr LEVEL "6" -> { (pat, e) } ] ]
   ;
   rec_flag:
     [ [ IDENT "rec" -> { true }
@@ -193,7 +194,7 @@ GRAMMAR EXTEND Gram
     [ [ IDENT "mutable" -> { true }
       | -> { false } ] ]
   ;
-  typ_param:
+  ltac2_typevar:
     [ [ "'"; id = Prim.ident -> { id } ] ]
   ;
   tactic_atom:
@@ -222,7 +223,7 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   tac2expr_in_env :
-    [ [ test_ltac1_env; ids = LIST0 locident; "|-"; e = tac2expr ->
+    [ [ test_ltac1_env; ids = LIST0 locident; "|-"; e = ltac2_expr ->
       { let check { CAst.v = id; CAst.loc = loc } =
           if Tac2env.is_constructor (Libnames.qualid_of_ident ?loc id) then
             CErrors.user_err ?loc Pp.(str "Invalid bound Ltac2 identifier " ++ Id.print id)
@@ -230,11 +231,11 @@ GRAMMAR EXTEND Gram
         let () = List.iter check ids in
         (ids, e)
       }
-      | tac = tac2expr -> { [], tac }
+      | tac = ltac2_expr -> { [], tac }
     ] ]
   ;
   let_clause:
-    [ [ binder = let_binder; ":="; te = tac2expr ->
+    [ [ binder = let_binder; ":="; te = ltac2_expr ->
       { let (pat, fn) = binder in
         let te = match fn with
         | None -> te
@@ -252,23 +253,23 @@ GRAMMAR EXTEND Gram
         | _ -> CErrors.user_err ~loc (str "Invalid pattern") }
     ] ]
   ;
-  tac2type:
+  ltac2_type:
     [ "5" RIGHTA
-      [ t1 = tac2type; "->"; t2 = tac2type -> { CAst.make ~loc @@ CTypArrow (t1, t2) } ]
+      [ t1 = ltac2_type; "->"; t2 = ltac2_type -> { CAst.make ~loc @@ CTypArrow (t1, t2) } ]
     | "2"
-      [ t = tac2type; "*"; tl = LIST1 tac2type LEVEL "1" SEP "*" ->
+      [ t = ltac2_type; "*"; tl = LIST1 ltac2_type LEVEL "1" SEP "*" ->
       { let tl = t :: tl in
         CAst.make ~loc @@ CTypRef (AbsKn (Tuple (List.length tl)), tl) } ]
     | "1" LEFTA
       [ t = SELF; qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, [t]) } ]
     | "0"
-      [ "(";  p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = OPT Prim.qualid ->
+      [ "(";  p = LIST1 ltac2_type LEVEL "5" SEP ","; ")"; qid = OPT Prim.qualid ->
         { match p, qid with
           | [t], None -> t
           | _, None -> CErrors.user_err ~loc (Pp.str "Syntax error")
           | ts, Some qid -> CAst.make ~loc @@ CTypRef (RelId qid, p)
         }
-      | id = typ_param -> { CAst.make ~loc @@ CTypVar (Name id) }
+      | id = ltac2_typevar -> { CAst.make ~loc @@ CTypVar (Name id) }
       | "_" -> { CAst.make ~loc @@ CTypVar Anonymous }
       | qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, []) }
       ]
@@ -284,7 +285,7 @@ GRAMMAR EXTEND Gram
     [ [ b = tac2pat LEVEL "0" -> { b } ] ]
   ;
   tac2def_body:
-    [ [ name = binder; it = LIST0 input_fun; ":="; e = tac2expr ->
+    [ [ name = binder; it = LIST0 input_fun; ":="; e = ltac2_expr ->
       { let e = if List.is_empty it then e else CAst.make ~loc @@ CTacFun (it, e) in
         (name, e) }
     ] ]
@@ -295,10 +296,10 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   tac2def_mut:
-    [ [ "Set"; qid = Prim.qualid; old = OPT [ "as"; id = locident -> { id } ]; ":="; e = tac2expr -> { StrMut (qid, old, e) } ] ]
+    [ [ "Set"; qid = Prim.qualid; old = OPT [ "as"; id = locident -> { id } ]; ":="; e = ltac2_expr -> { StrMut (qid, old, e) } ] ]
   ;
   tac2typ_knd:
-    [ [ t = tac2type -> { CTydDef (Some t) }
+    [ [ t = ltac2_type -> { CTydDef (Some t) }
       | "["; ".."; "]" -> { CTydOpn }
       | "["; t = tac2alg_constructors; "]" -> { CTydAlg t }
       | "{"; t = tac2rec_fields; "}"-> { CTydRec t } ] ]
@@ -309,7 +310,7 @@ GRAMMAR EXTEND Gram
   ;
   tac2alg_constructor:
     [ [ c = Prim.ident -> { (c, []) }
-      | c = Prim.ident; "("; args = LIST0 tac2type SEP ","; ")"-> { (c, args) } ] ]
+      | c = Prim.ident; "("; args = LIST0 ltac2_type SEP ","; ")"-> { (c, args) } ] ]
   ;
   tac2rec_fields:
     [ [ f = tac2rec_field; ";"; l = tac2rec_fields -> { f :: l }
@@ -318,7 +319,7 @@ GRAMMAR EXTEND Gram
       | -> { [] } ] ]
   ;
   tac2rec_field:
-    [ [ mut = mut_flag; id = Prim.ident; ":"; t = tac2type -> { (id, mut, t) } ] ]
+    [ [ mut = mut_flag; id = Prim.ident; ":"; t = ltac2_type -> { (id, mut, t) } ] ]
   ;
   tac2rec_fieldexprs:
     [ [ f = tac2rec_fieldexpr; ";"; l = tac2rec_fieldexprs -> { f :: l }
@@ -327,12 +328,12 @@ GRAMMAR EXTEND Gram
       | -> { [] } ] ]
   ;
   tac2rec_fieldexpr:
-    [ [ qid = Prim.qualid; ":="; e = tac2expr LEVEL "1" -> { RelId qid, e } ] ]
+    [ [ qid = Prim.qualid; ":="; e = ltac2_expr LEVEL "1" -> { RelId qid, e } ] ]
   ;
   tac2typ_prm:
     [ [ -> { [] }
-      | id = typ_param -> { [CAst.make ~loc id] }
-      | "("; ids = LIST1 [ id = typ_param -> { CAst.make ~loc id } ] SEP "," ;")" -> { ids }
+      | id = ltac2_typevar -> { [CAst.make ~loc id] }
+      | "("; ids = LIST1 [ id = ltac2_typevar -> { CAst.make ~loc id } ] SEP "," ;")" -> { ids }
     ] ]
   ;
   tac2typ_def:
@@ -350,7 +351,7 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   tac2def_ext:
-    [ [ "@"; IDENT "external"; id = locident; ":"; t = tac2type LEVEL "5"; ":=";
+    [ [ "@"; IDENT "external"; id = locident; ":"; t = ltac2_type LEVEL "5"; ":=";
         plugin = Prim.string; name = Prim.string ->
       { let ml = { mltac_plugin = plugin; mltac_tactic = name } in
         StrPrm (id, t, ml) }
@@ -376,7 +377,7 @@ GRAMMAR EXTEND Gram
   ;
   tac2def_syn:
     [ [ "Notation"; toks = LIST1 ltac2_scope; n = syn_level; ":=";
-        e = tac2expr ->
+        e = ltac2_expr ->
         { StrSyn (toks, n, e) }
     ] ]
   ;
@@ -654,15 +655,15 @@ GRAMMAR EXTEND Gram
     [ [ r = oriented_rewriter -> { r } ] ]
   ;
   tactic_then_last:
-    [ [ "|"; lta = LIST0 (OPT tac2expr LEVEL "6") SEP "|" -> { lta }
+    [ [ "|"; lta = LIST0 (OPT ltac2_expr LEVEL "6") SEP "|" -> { lta }
       | -> { [] }
     ] ]
   ;
   for_each_goal:
-    [ [ ta = tac2expr; "|"; tg = for_each_goal -> { let (first,last) = tg in (Some ta :: first, last) }
-      | ta = tac2expr; ".."; l = tactic_then_last -> { ([], Some (Some ta, l)) }
+    [ [ ta = ltac2_expr; "|"; tg = for_each_goal -> { let (first,last) = tg in (Some ta :: first, last) }
+      | ta = ltac2_expr; ".."; l = tactic_then_last -> { ([], Some (Some ta, l)) }
       | ".."; l = tactic_then_last -> { ([], Some (None, l)) }
-      | ta = tac2expr -> { ([Some ta], None) }
+      | ta = ltac2_expr -> { ([Some ta], None) }
       | "|"; tg = for_each_goal -> { let (first,last) = tg in (None :: first, last) }
       | -> { ([None], None) }
     ] ]
@@ -725,7 +726,7 @@ GRAMMAR EXTEND Gram
       | pat = Constr.cpattern -> { CAst.make ~loc @@ QConstrMatchPattern pat } ] ]
   ;
   match_rule:
-    [ [ mp = match_pattern; "=>"; tac = tac2expr ->
+    [ [ mp = match_pattern; "=>"; tac = ltac2_expr ->
         { CAst.make ~loc @@ (mp, tac) }
     ] ]
   ;
@@ -748,7 +749,7 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   gmatch_rule:
-    [ [ mp = gmatch_pattern; "=>"; tac = tac2expr ->
+    [ [ mp = gmatch_pattern; "=>"; tac = ltac2_expr ->
         { CAst.make ~loc @@ (mp, tac) }
     ] ]
   ;
@@ -789,7 +790,7 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   by_tactic:
-    [ [ "by"; tac = tac2expr -> { Some tac }
+    [ [ "by"; tac = ltac2_expr -> { Some tac }
       | -> { None }
     ] ]
   ;
@@ -813,7 +814,7 @@ END
 (*
 GRAMMAR EXTEND Gram
   Pcoq.Constr.term: LEVEL "0"
-    [ [ IDENT "ltac2"; ":"; "("; tac = tac2expr; ")" ->
+    [ [ IDENT "ltac2"; ":"; "("; tac = ltac2_expr; ")" ->
       { let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in
         CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg)) }
       | test_ampersand_ident; "&"; id = Prim.ident ->
@@ -858,7 +859,7 @@ let rules = [
   Pcoq.(
     Production.make
       (Rule.stop ++ Symbol.token (PIDENT (Some "ltac2")) ++ Symbol.token (PKEYWORD ":") ++
-       Symbol.token (PKEYWORD "(") ++ Symbol.nterm tac2expr ++ Symbol.token (PKEYWORD ")"))
+       Symbol.token (PKEYWORD "(") ++ Symbol.nterm ltac2_expr ++ Symbol.token (PKEYWORD ")"))
     begin fun _ tac _ _ _ loc ->
       let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in
       CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg))
@@ -890,7 +891,7 @@ END
 
 VERNAC ARGUMENT EXTEND ltac2_expr
 PRINTED BY { pr_ltac2expr }
-| [ tac2expr(e) ] -> { e }
+| [ _ltac2_expr(e) ] -> { e }
 END
 
 {
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 3ce50865c0..5d49d1635c 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1541,12 +1541,12 @@ end
 let () = add_scope "tactic" begin function
 | [] ->
   (* Default to level 5 parsing *)
-  let scope = Pcoq.Symbol.nterml tac2expr "5" in
+  let scope = Pcoq.Symbol.nterml ltac2_expr "5" in
   let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | [SexprInt {loc;v=n}] as arg ->
   let () = if n < 0 || n > 6 then scope_fail "tactic" arg in
-  let scope = Pcoq.Symbol.nterml tac2expr (string_of_int n) in
+  let scope = Pcoq.Symbol.nterml ltac2_expr (string_of_int n) in
   let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | arg -> scope_fail "tactic" arg
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 03789fff6c..eebd6635fa 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -24,7 +24,8 @@ open Tac2intern
 
 module Pltac =
 struct
-let tac2expr = Pcoq.Entry.create "tac2expr"
+let ltac2_expr = Pcoq.Entry.create "ltac2_expr"
+let tac2expr = ltac2_expr
 let tac2expr_in_env = Pcoq.Entry.create "tac2expr_in_env"
 
 let q_ident = Pcoq.Entry.create "q_ident"
@@ -643,7 +644,7 @@ let perform_notation syn st =
   | Some lev -> Some (string_of_int lev)
   in
   let rule = (lev, None, [rule]) in
-  ([Pcoq.ExtendRule (Pltac.tac2expr, {Pcoq.pos=None; data=[rule]})], st)
+  ([Pcoq.ExtendRule (Pltac.ltac2_expr, {Pcoq.pos=None; data=[rule]})], st)
 
 let ltac2_notation =
   Pcoq.create_grammar_command "ltac2-notation" perform_notation
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index 2f053df2d0..782968c6e1 100644
--- a/user-contrib/Ltac2/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
@@ -63,7 +63,9 @@ val backtrace : backtrace Exninfo.t
 
 module Pltac :
 sig
+val ltac2_expr : raw_tacexpr Pcoq.Entry.t
 val tac2expr : raw_tacexpr Pcoq.Entry.t
+  [@@deprecated "Deprecated in 8.13; use 'ltac2_expr' instead"]
 val tac2expr_in_env : (Id.t CAst.t list * raw_tacexpr) Pcoq.Entry.t
 
 (** Quoted entries. To be used for complex notations. *)