diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 352d1297a1..2e7e804aab 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -298,7 +298,7 @@ let rec detype avoid env t = | IsConst (sp,cl) -> detype_reference avoid env (ConstRef sp) cl | IsEvar (ev,cl) -> - let f = RRef (dummy_loc, EvarRef ev) in + let f = REvar (dummy_loc, ev) in RApp (dummy_loc, f, List.map (detype avoid env) (Array.to_list cl)) | IsMutInd (ind_sp,cl) -> detype_reference avoid env (IndRef ind_sp) cl |