diff options
| author | Gaëtan Gilbert | 2019-06-13 15:39:43 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-01 13:06:22 +0200 |
| commit | 2ded4c25e532c5dfca0483c211653768ebed01a7 (patch) | |
| tree | a04b2f787490c8971590e6bdf7dd1ec4220e0290 /pretyping/vnorm.ml | |
| parent | b017e302f69f20fc4fc3d4088a305194f6c387fa (diff) | |
UIP in SProp
Diffstat (limited to 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 37c34d55cf..efe1efd74e 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -261,6 +261,12 @@ and nf_stk ?from:(from=0) env sigma c t stk = nf_stk env sigma (mkApp(fa,[|c|])) (subst1 c codom) stk | Zswitch sw :: stk -> assert (from = 0) ; + let ci = sw.sw_annot.Vmvalues.ci in + let () = if Typeops.should_invert_case env ci then + (* TODO implement case inversion readback (properly reducing + it is a problem for the kernel) *) + CErrors.user_err Pp.(str "VM compute readback of case inversion not implemented.") + in let ((mind,_ as ind), u), allargs = find_rectype_a env t in let (mib,mip) = Inductive.lookup_mind_specif env ind in let nparams = mib.mind_nparams in @@ -280,8 +286,7 @@ and nf_stk ?from:(from=0) env sigma c t stk = in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type p realargs c in - let ci = sw.sw_annot.Vmvalues.ci in - nf_stk env sigma (mkCase(ci, p, c, branchs)) tcase stk + nf_stk env sigma (mkCase(ci, p, NoInvert, c, branchs)) tcase stk | Zproj p :: stk -> assert (from = 0) ; let p' = Projection.make p true in |