diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-19 16:17:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-19 16:17:40 +0200 |
| commit | c37881f3d64a6db0d7414eb18adfa4de6b64d4b1 (patch) | |
| tree | 873e3f19156ed947e539eddcf5405e64f15e0194 /pretyping | |
| parent | a5722cc823dcf13594098dd21813feaaaf893bf0 (diff) | |
| parent | bc103cc493b2127f8a570bcf2e8be94378d79a55 (diff) | |
Merge PR #6754: Better elaboration of pattern-matchings on primitive projections
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 2 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 20 |
2 files changed, 12 insertions, 10 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 0dd3c5944..93ca9dc5e 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1425,7 +1425,7 @@ and match_current pb (initial,tomatch) = let ci = make_case_info pb.env (fst mind) pb.casestyle in let pred = nf_betaiota pb.env !(pb.evdref) pred in let case = - make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals + make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals in let _ = Evarutil.evd_comb1 (Typing.type_of pb.env) pb.evdref pred in Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred; diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 1a790be64..1003f86c5 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -356,8 +356,8 @@ let make_case_or_project env sigma indf ci pred c branches = | None -> (mkCase (ci, pred, c, branches)) | Some ps -> assert(Array.length branches == 1); + let na, ty, t = destLambda sigma pred in let () = - let _, _, t = destLambda sigma pred in let (ind, _), _ = dest_ind_family indf in let mib, _ = Inductive.lookup_mind_specif env ind in if (* dependent *) not (Vars.noccurn sigma 1 t) && @@ -368,16 +368,18 @@ let make_case_or_project env sigma indf ci pred c branches = in let branch = branches.(0) in let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in - let n, subst = + let n, len, ctx = List.fold_right - (fun decl (i, subst) -> + (fun decl (i, j, ctx) -> match decl with - | LocalAssum (na, t) -> - let t = mkProj (Projection.make ps.(i) true, c) in - (i + 1, t :: subst) - | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst)) - ctx (0, []) - in Vars.substl subst br + | LocalAssum (na, ty) -> + let t = mkProj (Projection.make ps.(i) true, mkRel j) in + (i + 1, j + 1, LocalDef (na, t, Vars.liftn 1 j ty) :: ctx) + | LocalDef (na, b, ty) -> + (i, j + 1, LocalDef (na, Vars.liftn 1 j b, Vars.liftn 1 j ty) :: ctx)) + ctx (0, 1, []) + in + mkLetIn (na, c, ty, it_mkLambda_or_LetIn (Vars.liftn 1 (Array.length ps + 1) br) ctx) (* substitution in a signature *) |