diff options
| author | coqbot-app[bot] | 2021-01-06 13:04:20 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-06 13:04:20 +0000 |
| commit | 30f497eaf34f2cf641c3fe854fc9066ae19eea67 (patch) | |
| tree | 473734cdc4ea6769de9a5563a0e9e6eeb56dce20 /kernel/inferCumulativity.ml | |
| parent | 960178db193c8a78b9414abad13536693ee5b9b8 (diff) | |
| parent | a95654a21c350f19ad0da67713359cbf6c49e95a (diff) | |
Merge PR #13563: Revival of #9710 (Compact kernel representation of pattern-matching)
Reviewed-by: mattam82
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: jfehrle
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 |