diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index b5d825e843..af237d1d12 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -630,7 +630,7 @@ let check_one_fix renv recpos def = (* The cases below simply check recursively the condition on the subterms *) - | Cast (a,b) -> + | Cast (a,_, b) -> List.for_all (check_rec_call renv) (a::b::l) | Lambda (x,a,b) -> |