Prim.pattern_ident takes a location and its synonymous pattern_identref is deprecated.

6 files changed, 14 insertions, 12 deletions

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index fb5d7cc244..8d0bcd1ee6 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -17,6 +17,11 @@
   was instead intended. If cancelling the breaking role of cuts in the
   box was intended, turn `h n c` into `h c`.
 
+### Grammar entries
+
+- `Prim.pattern_identref` is deprecated, use `Prim.pattern_ident`
+  which now returns a located identifier.
+
 ## Changes between Coq 8.11 and Coq 8.12
 
 ### Code formatting
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 931ffccb27..644493a010 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -154,7 +154,7 @@ GRAMMAR EXTEND Gram
     | "10" LEFTA
       [ f = operconstr; args = LIST1 appl_arg -> { CAst.make ~loc @@ CApp((None,f),args) }
       | "@"; f = global; i = univ_instance; args = LIST0 NEXT -> { CAst.make ~loc @@ CAppExpl((None,f,i),args) }
-      | "@"; lid = pattern_identref; args = LIST1 identref ->
+      | "@"; lid = pattern_ident; args = LIST1 identref ->
         { let { CAst.loc = locid; v = id } = lid in
           let args = List.map (fun x -> CAst.make @@ CRef (qualid_of_ident ?loc:x.CAst.loc x.CAst.v, None), None) args in
           CAst.make ~loc @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) } ]
@@ -262,8 +262,8 @@ GRAMMAR EXTEND Gram
       | s = string -> { CAst.make ~loc @@ CPrim (String s) }
       | "_"      -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) }
       | "?"; "["; id = identref; "]"  -> { CAst.make ~loc @@  CHole (None, IntroIdentifier id.CAst.v, None) }
-      | "?"; "["; id = pattern_ident; "]"  -> { CAst.make ~loc @@  CHole (None, IntroFresh id, None) }
-      | id = pattern_identref; inst = evar_instance -> { CAst.make ~loc @@ CEvar(id,inst) } ] ]
+      | "?"; "["; id = pattern_ident; "]"  -> { CAst.make ~loc @@  CHole (None, IntroFresh id.CAst.v, None) }
+      | id = pattern_ident; inst = evar_instance -> { CAst.make ~loc @@ CEvar(id,inst) } ] ]
   ;
   inst:
     [ [ id = identref; ":="; c = lconstr -> { (id,c) } ] ]
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index 270662b824..8069f049fd 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -47,7 +47,7 @@ GRAMMAR EXTEND Gram
   GLOBAL:
     bignat bigint natural integer identref name ident var preident
     fullyqualid qualid reference dirpath ne_lstring
-    ne_string string lstring pattern_ident pattern_identref by_notation
+    ne_string string lstring pattern_ident by_notation
     smart_global bar_cbrace strategy_level;
   preident:
     [ [ s = IDENT -> { s } ] ]
@@ -56,10 +56,7 @@ GRAMMAR EXTEND Gram
     [ [ s = IDENT -> { Id.of_string s } ] ]
   ;
   pattern_ident:
-    [ [ LEFTQMARK; id = ident -> { id } ] ]
-  ;
-  pattern_identref:
-    [ [ id = pattern_ident -> { CAst.make ~loc id } ] ]
+    [ [ LEFTQMARK; id = ident -> { CAst.make ~loc id } ] ]
   ;
   var: (* as identref, but interpret as a term identifier in ltac *)
     [ [ id = ident -> { CAst.make ~loc id } ] ]
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 723f08413e..fa7de40a30 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -286,7 +286,7 @@ module Prim =
     let univ_decl = Entry.create "univ_decl"
     let ident_decl = Entry.create "ident_decl"
     let pattern_ident = Entry.create "pattern_ident"
-    let pattern_identref = Entry.create "pattern_identref"
+    let pattern_identref = pattern_ident (* To remove in 8.14 *)
 
     (* A synonym of ident - maybe ident will be located one day *)
     let base_ident = Entry.create "base_ident"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index ae9a7423c2..fa223367f7 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -156,8 +156,8 @@ module Prim :
     val identref : lident Entry.t
     val univ_decl : universe_decl_expr Entry.t
     val ident_decl : ident_decl Entry.t
-    val pattern_ident : Id.t Entry.t
-    val pattern_identref : lident Entry.t
+    val pattern_ident : lident Entry.t
+    val pattern_identref : lident Entry.t [@@ocaml.deprecated "Use Prim.pattern_identref"]
     val base_ident : Id.t Entry.t
     val bignat : string Entry.t
     val natural : int Entry.t
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index e51b1f051d..c186a83a5c 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -280,7 +280,7 @@ GRAMMAR EXTEND Gram
       | "[="; tc = intropatterns; "]" -> { IntroInjection tc } ] ]
   ;
   naming_intropattern:
-    [ [ prefix = pattern_ident -> { IntroFresh prefix }
+    [ [ prefix = pattern_ident -> { IntroFresh prefix.CAst.v }
       | "?" -> { IntroAnonymous }
       | id = ident -> { IntroIdentifier id } ] ]
   ;