diff options
Diffstat (limited to 'kernel/inferCumulativity.ml')
| -rw-r--r-- | kernel/inferCumulativity.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml index d02f92ef26..50c3ba1cc6 100644 --- a/kernel/inferCumulativity.ml +++ b/kernel/inferCumulativity.ml @@ -198,7 +198,9 @@ let rec infer_fterm cv_pb infos variances hd stk = let variances = infer_vect infos variances elems in infer_stack infos variances stk - | FCaseInvert (_,p,_,_,br,e) -> + | FCaseInvert (ci, u, pms, p, _, _, br, e) -> + let mib = Environ.lookup_mind (fst ci.ci_ind) (info_env (fst infos)) in + let (_, p, _, _, br) = Inductive.expand_case_specif mib (ci, u, pms, p, NoInvert, mkProp, br) in let infer c variances = infer_fterm CONV infos variances (mk_clos e c) [] in let variances = infer p variances in Array.fold_right infer br variances @@ -217,7 +219,10 @@ and infer_stack infos variances (stk:CClosure.stack) = | Zfix (fx,a) -> let variances = infer_fterm CONV infos variances fx [] in infer_stack infos variances a - | ZcaseT (_, p, br, e) -> + | ZcaseT (ci,u,pms,p,br,e) -> + let dummy = mkProp in + let case = (ci, u, pms, p, NoInvert, dummy, br) in + let (_, p, _, _, br) = Inductive.expand_case (info_env (fst infos)) case in let variances = infer_fterm CONV infos variances (mk_clos e p) [] in infer_vect infos variances (Array.map (mk_clos e) br) | Zshift _ -> variances |