From b7c9ba2c678228593450ecdf272ff71facbc6a6e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 27 Sep 2020 10:48:29 +0200
Subject: Add location in existential variable names (CEvar/GEvar).

---
 printing/proof_diffs.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'printing/proof_diffs.ml')

diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index 43f70dfecc..fab44e8875 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -511,12 +511,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;
-- 
cgit v1.2.3