diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 192bb69d66..0c80c3a414 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -627,7 +627,9 @@ let branches_specif renv c_spec ci = let check_inductive_codomain env p = let absctx, ar = dest_lam_assum env p in + let env = push_rel_context absctx env in let arctx, s = dest_prod_assum env ar in + let env = push_rel_context arctx env in let i,l' = decompose_app (whd_betadeltaiota env s) in isInd i |