aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/detyping.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/detyping.ml')
-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) ->