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 /pretyping/patternops.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 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index b259945d9e..47097a0e32 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -202,7 +202,8 @@ let pattern_of_constr env sigma t = | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false | _ -> PMeta None) - | Case (ci,p,_,a,br) -> + | Case (ci, u, pms, p, iv, a, br) -> + let (ci, p, iv, a, br) = Inductive.expand_case env (ci, u, pms, p, iv, a, br) in let cip = { cip_style = ci.ci_pp_info.style; cip_ind = Some ci.ci_ind; @@ -213,7 +214,7 @@ let pattern_of_constr env sigma t = (i, ci.ci_pp_info.cstr_tags.(i), pattern_of_constr env c) in PCase (cip, pattern_of_constr env p, pattern_of_constr env a, - Array.to_list (Array.mapi branch_of_constr br)) + Array.to_list (Array.mapi branch_of_constr br)) | Fix (lni,(lna,tl,bl)) -> let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in let env' = Array.fold_left2 push env lna tl in |