diff options
| -rw-r--r-- | kernel/indtypes.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index a695372314..9a11e47dc3 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -598,8 +598,12 @@ let allowed_sorts issmall isunit s = | InProp -> logical_sorts let fold_inductive_blocks f = - Array.fold_left (fun acc (_,_,lc,(arsign,_)) -> - f (Array.fold_left f acc lc) (it_mkProd_or_LetIn (* dummy *) mkSet arsign)) + let concl = function + | Inr _ -> mkSet (* dummy *) + | Inl (_,ar,_) -> ar + in + Array.fold_left (fun acc (_,_,lc,(arsign,ar)) -> + f (Array.fold_left f acc lc) (it_mkProd_or_LetIn (concl ar) arsign)) let used_section_variables env inds = let ids = fold_inductive_blocks |