aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--pretyping/cases.ml2
-rw-r--r--pretyping/inductiveops.ml20
-rw-r--r--test-suite/success/letproj.v2
3 files changed, 14 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 b1ab2d2b7..f839d5b98 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 *)
diff --git a/test-suite/success/letproj.v b/test-suite/success/letproj.v
index de2857b43..2f0d8bf8c 100644
--- a/test-suite/success/letproj.v
+++ b/test-suite/success/letproj.v
@@ -7,3 +7,5 @@ Definition test (A : Type) (f : Foo A) :=
Scheme foo_case := Case for Foo Sort Type.
+Definition test' (A : Type) (f : Foo A) :=
+ let 'Build_Foo _ x y := f in x.