Merge PR #13099: Locating pattern identifiers (?id) by default at parsing time and use location in some typing error messages

Reviewed-by: ppedrot

2 files changed, 5 insertions, 5 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 267f5e0b5f..4200268acc 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -227,11 +227,11 @@ let tag_var = tag Tag.variable
 
   let pr_evar pr id l =
     hov 0 (
-      tag_evar (str "?" ++ pr_id id) ++
+      tag_evar (str "?" ++ pr_lident id) ++
         (match l with
           | [] -> mt()
           | l ->
-            let f (id,c) = pr_id id ++ str ":=" ++ pr ltop c in
+            let f (id,c) = pr_lident id ++ str ":=" ++ pr ltop c in
             str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}"))
 
   let las = lapp
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index dd372ecb0f..b2ebc61b4e 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -514,12 +514,12 @@ let match_goals ot nt =
     | CHole (k,naming,solve), CHole (k2,naming2,solve2) -> ()
     | CPatVar _, CPatVar _ -> ()
     | CEvar (n,l), CEvar (n2,l2) ->
-      let oevar = if ogname = "" then Id.to_string n else ogname in
-      nevar_to_oevar := CString.Map.add (Id.to_string n2) oevar !nevar_to_oevar;
+      let oevar = if ogname = "" then Id.to_string n.CAst.v else ogname in
+      nevar_to_oevar := CString.Map.add (Id.to_string n2.CAst.v) oevar !nevar_to_oevar;
       iter2  (fun x x2 -> let (_, g) = x and (_, g2) = x2 in constr_expr ogname g g2)  l l2
     | CEvar (n,l), nt' ->
       (* pass down the old goal evar name *)
-      match_goals_r (Id.to_string n) nt' nt'
+      match_goals_r (Id.to_string n.CAst.v) nt' nt'
     | CSort s, CSort s2 -> ()
     | CCast (c,c'), CCast (c2,c'2) ->
       constr_expr ogname c c2;