diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-17 13:58:52 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-17 13:58:52 +0200 |
| commit | 239cf334fcc844f06a9e6ea2e6745d2fa8915325 (patch) | |
| tree | e2cb479303069c571be17015734eca6dbb8845a3 /pretyping | |
| parent | 251218905daea0838a3738466afa1c278bb3e81b (diff) | |
Re-displaying evar instances in debugger.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 1e5d784ea..605d59135 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -499,7 +499,11 @@ let rec detype flags avoid env sigma t = isRelN n c with Not_found -> isVarId id c) (Evd.find sigma evk) cl - with Not_found -> Id.of_string ("X" ^ string_of_int (Evar.repr evk)), [] in + with Not_found -> + Id.of_string ("X" ^ string_of_int (Evar.repr evk)), + (List.map_i (fun i c -> (Id.of_string ("A" ^ string_of_int i),c)) + 1 (Array.to_list cl)) + in GEvar (dl,id, List.map (on_snd (detype flags avoid env sigma)) l) | Ind (ind_sp,u) -> |