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 dd3022764..a02cf96a6 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -282,7 +282,7 @@ let rec detype avoid env t = | IsProd (na,ty,c) -> detype_binder BProd avoid env na ty c | IsLambda (na,ty,c) -> detype_binder BLambda avoid env na ty c | IsLetIn (na,b,_,c) -> detype_binder BLetIn avoid env na b c - | IsAppL (f,args) -> + | IsApp (f,args) -> RApp (dummy_loc,detype avoid env f,array_map_to_list (detype avoid env) args) | IsConst (sp,cl) -> RRef(dummy_loc,RConst(sp,Array.map (detype avoid env) cl)) |