diff options
| -rw-r--r-- | kernel/indtypes.ml | 17 | ||||
| -rw-r--r-- | test-suite/success/primitiveproj.v | 15 |
2 files changed, 23 insertions, 9 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 351de9ee88..f08f0b7bbb 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -654,13 +654,12 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params matching with a parameter context. *) let indty, paramsletsubst = let subst, inst = - List.fold_right - (fun (na, b, t) (subst, inst) -> + List.fold_right_i + (fun i (na, b, t) (subst, inst) -> match b with - | None -> (mkRel 1 :: List.map (lift 1) subst, - mkRel 1 :: List.map (lift 1) inst) - | Some b -> (substl subst b) :: subst, List.map (lift 1) inst) - paramslet ([], []) + | None -> (mkRel i :: subst, mkRel i :: inst) + | Some b -> (substl subst b) :: subst, inst) + 1 paramslet ([], []) in let subst = (* For the record parameter: *) mkRel 1 :: List.map (lift 1) subst @@ -690,8 +689,10 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params in let projections (na, b, t) (i, j, kns, pbs, subst, letsubst) = match b with - | Some c -> (i, j+1, kns, pbs, substl subst c :: subst, - substl letsubst c :: subst) + | Some c -> + let c = liftn 1 j c in + (i, j+1, kns, pbs, substl subst c :: subst, + substl letsubst c :: letsubst) | None -> match na with | Name id -> diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 125615c535..281d707cb3 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -194,4 +194,17 @@ Record wrap (A : Type) := { unwrap : A; unwrap2 : A }. Definition term (x : wrap nat) := x.(unwrap). Definition term' (x : wrap nat) := let f := (@unwrap2 nat) in f x. Recursive Extraction term term'. -(*Unset Printing Primitive Projection Parameters.*)
\ No newline at end of file +(*Unset Printing Primitive Projection Parameters.*) + +(* Primitive projections in the presence of let-ins (was not failing in beta3)*) + +Set Primitive Projections. +Record s (x:nat) (y:=S x) := {c:=x; d:x=c}. +Lemma f : 0=1. +Proof. +Fail apply d. +(* +split. +reflexivity. +Qed. +*) |