diff options
Diffstat (limited to 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 0eefa24423..ee1bfe4d60 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -263,7 +263,7 @@ let rec strip_head_cast c = match kind_of_term c with let rec collapse_rec f cl2 = match kind_of_term f with | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) | Cast (c,_) -> collapse_rec c cl2 - | _ -> if cl2 = [||] then f else mkApp (f,cl2) + | _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2) in collapse_rec f cl | Cast (c,t) -> strip_head_cast c |