diff options
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 6869f9c47e..0cad192332 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -672,9 +672,11 @@ let rec extract_term env sg mle mlt c args = (* we unify it with an fresh copy of the stored type of [Rel n]. *) let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n) in extract_app env sg mle mlt extract_rel args - | Case ({ci_ind=ip},_,iv,c0,br) -> - (* If invert_case then this is a match that will get erased later, but right now we don't care. *) - extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args + | Case (ci, u, pms, r, iv, c0, br) -> + (* If invert_case then this is a match that will get erased later, but right now we don't care. *) + let (ip, r, iv, c0, br) = EConstr.expand_case env sg (ci, u, pms, r, iv, c0, br) in + let ip = ci.ci_ind in + extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args | Fix ((_,i),recd) -> extract_app env sg mle mlt (extract_fix env sg mle i recd) args | CoFix (i,recd) -> @@ -1078,9 +1080,13 @@ let fake_match_projection env p = let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg:arg lab in fold (arg+1) (j+1) (mkProj (Projection.make kn false, mkRel 1)::subst) rem else - let p = mkLambda (x, lift 1 indty, liftn 1 2 ty) in - let branch = lift 1 (it_mkLambda_or_LetIn (mkRel (List.length ctx - (j-1))) ctx) in - let body = mkCase (ci, p, NoInvert, mkRel 1, [|branch|]) in + let p = ([|x|], liftn 1 2 ty) in + let branch = + let nas = Array.of_list (List.rev_map Context.Rel.Declaration.get_annot ctx) in + (nas, mkRel (List.length ctx - (j - 1))) + in + let params = Context.Rel.to_extended_vect mkRel 1 paramslet in + let body = mkCase (ci, u, params, p, NoInvert, mkRel 1, [|branch|]) in it_mkLambda_or_LetIn (mkLambda (x,indty,body)) mib.mind_params_ctxt | LocalDef (_,c,t) :: rem -> let c = liftn 1 j c in |