diff options
| author | Pierre-Marie Pédrot | 2020-07-11 13:23:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-07-11 13:23:55 +0200 |
| commit | ed8a428267088ef3e6010c545c449117353a1179 (patch) | |
| tree | 65d4a08de31039351bb14b0592fef1ffcff9580f /pretyping/nativenorm.ml | |
| parent | c412b32707a296a6b17292782ed1194413353387 (diff) | |
| parent | aacfda0817557e0e3530966282a7ba1b303590b2 (diff) | |
Merge PR #12646: Correctly readback blocked CaseInvert matches in VM/native
Reviewed-by: ppedrot
Diffstat (limited to 'pretyping/nativenorm.ml')
| -rw-r--r-- | pretyping/nativenorm.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 30e1dc0611..3f68e3c78f 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -318,13 +318,12 @@ and nf_atom_type env sigma atom = | Avar id -> mkVar id, Typeops.type_of_variable env id | Acase(ans,accu,p,bs) -> - let () = if Typeops.should_invert_case env ans.asw_ci then - (* TODO implement case inversion readback (properly reducing - it is a problem for the kernel) *) - CErrors.user_err Pp.(str "Native compute readback of case inversion not implemented.") - in let a,ta = nf_accu_type env sigma accu in let ((mind,_),u as ind),allargs = find_rectype_a env ta in + let iv = if Typeops.should_invert_case env ans.asw_ci then + CaseInvert {univs=u; args=allargs} + else NoInvert + in let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in let nparams = mib.mind_nparams in let params,realargs = Array.chop nparams allargs in @@ -344,7 +343,7 @@ and nf_atom_type env sigma atom = in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type p realargs a in - mkCase(ans.asw_ci, p, NoInvert, a, branchs), tcase + mkCase(ans.asw_ci, p, iv, a, branchs), tcase | Afix(tt,ft,rp,s) -> let tt = Array.map (fun t -> nf_type_sort env sigma t) tt in let tt = Array.map fst tt and rt = Array.map snd tt in |