diff options
Diffstat (limited to 'kernel/inductive.ml')
-rw-r--r-- | kernel/inductive.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 7b2d92716..3c4c2796e 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -990,6 +990,10 @@ let check_one_fix renv recpos trees def = | (Ind _ | Construct _) -> List.iter (check_rec_call renv []) l + | Proj (p, c) -> + List.iter (check_rec_call renv []) l; + check_rec_call renv [] c + | Var id -> begin let open Context.Named.Declaration in @@ -1009,8 +1013,6 @@ let check_one_fix renv recpos trees def = | (Evar _ | Meta _) -> () | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *) - - | Proj (p, c) -> check_rec_call renv [] c and check_nested_fix_body renv decr recArgsDecrArg body = if Int.equal decr 0 then |