diff options
Diffstat (limited to 'pretyping/detyping.ml')
-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) -> |