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 /pretyping/detyping.ml | |
| parent | 2cf0287c9c863d7969fb5d4e85b7ca538dd103c2 (diff) | |
Add location in existential variable names (CEvar/GEvar).
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 503035c6c3..c5df5d7968 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -715,9 +715,9 @@ and detype_r d flags avoid env sigma t = (* Meta in constr are not user-parsable and are mapped to Evar *) if n = Constr_matching.special_meta then (* Using a dash to be unparsable *) - GEvar (Id.of_string_soft "CONTEXT-HOLE", []) + GEvar (CAst.make @@ Id.of_string_soft "CONTEXT-HOLE", []) else - GEvar (Id.of_string_soft ("M" ^ string_of_int n), []) + GEvar (CAst.make @@ Id.of_string_soft ("M" ^ string_of_int n), []) | Var id -> (* Discriminate between section variable and non-section variable *) (try let _ = Global.lookup_named id in GRef (GlobRef.VarRef id, None) @@ -793,7 +793,7 @@ and detype_r d flags avoid env sigma t = Id.of_string ("X" ^ string_of_int (Evar.repr evk)), (List.map (fun c -> (CAst.make @@ Id.of_string "__",c)) cl) in - GEvar (id, + GEvar (CAst.make id, List.map (on_snd (detype d flags avoid env sigma)) l) | Ind (ind_sp,u) -> GRef (GlobRef.IndRef ind_sp, detype_instance sigma u) |