diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-07 07:20:34 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-18 14:18:13 +0100 |
commit | c71aa6bd368b801bb17d4da69d1ab1e2bd7cbf39 (patch) | |
tree | f5723156276688c3be4221521a218d1f7b818db1 | |
parent | c4fef5b9d2be739cad030131fd6fc4c07d5e2e08 (diff) |
Fixing logical bugs in the presence of let-ins in computiong primitive
projections.
- lift accounting for the record missing in computing the subst from
fields to projections of the record
- substitution for parameters should not lift the local definitions
- typo in building the latter (subst -> letsubst)
-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 351de9ee8..f08f0b7bb 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 125615c53..281d707cb 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. +*) |