aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-17 13:58:52 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-17 13:58:52 +0200
commit239cf334fcc844f06a9e6ea2e6745d2fa8915325 (patch)
treee2cb479303069c571be17015734eca6dbb8845a3 /pretyping
parent251218905daea0838a3738466afa1c278bb3e81b (diff)
Re-displaying evar instances in debugger.
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/detyping.ml6
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) ->