diff options
| author | Hugo Herbelin | 2020-09-27 10:48:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-10 22:13:59 +0200 |
| commit | b7c9ba2c678228593450ecdf272ff71facbc6a6e (patch) | |
| tree | c652e8bd90a7281089ce5c9686892220ddf9ca6d /printing | |
| parent | 2cf0287c9c863d7969fb5d4e85b7ca538dd103c2 (diff) | |
Add location in existential variable names (CEvar/GEvar).
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 2 | ||||
| -rw-r--r-- | printing/proof_diffs.ml | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 30335d9826..4200268acc 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -227,7 +227,7 @@ 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 -> 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; |