diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/typeops.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index ce28a60a8..860153ef4 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -540,7 +540,10 @@ let rec check_subterm_rec_meta env sigma vectn k def = (array_for_all (check_rec_call env n lst) typarray) && (array_for_all - (check_rec_call env (n+nbfix) (map_lift_fst_n nbfix lst)) + (check_rec_call + (push_rec_types recdef env) + (n+nbfix) + (map_lift_fst_n nbfix lst)) bodies) else let theDecrArg = List.nth l decrArg in @@ -554,7 +557,10 @@ let rec check_subterm_rec_meta env sigma vectn k def = (array_for_all (check_rec_call env n lst) typarray) && (array_for_all - (check_rec_call env (n+nbfix) (map_lift_fst_n nbfix lst)) + (check_rec_call + (push_rec_types recdef env) + (n+nbfix) + (map_lift_fst_n nbfix lst)) bodies) else let theBody = bodies.(i) in |