aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-09-10 12:56:12 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-09-10 13:01:24 +0200
commit6624459e492164b3d189e3518864379ff985bf8c (patch)
tree9fc004c5f25927f671667d0cf5475061b306e1f0 /pretyping
parentc2fa953889cf7bcef9c369d175e156855ac0be2e (diff)
Fix generation of inductive elimination principle for primitive records.
Let r.(p) be a strict subterm of r during the guardness check.
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/indrec.ml25
1 files changed, 21 insertions, 4 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 54f76fa33..0cbfa7597 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -378,10 +378,27 @@ let mis_make_indrec env sigma listdepkind mib u =
(Anonymous,depind',concl))
arsign'
in
- it_mkLambda_or_LetIn_name env
- (mkCase (ci, pred,
- mkRel 1,
- branches))
+ let obj =
+ let projs = get_projections env indf in
+ match projs with
+ | None -> (mkCase (ci, pred,
+ mkRel 1,
+ branches))
+ | Some ps ->
+ let branch = branches.(0) in
+ let ctx, br = decompose_lam_assum branch in
+ let n, subst =
+ List.fold_right (fun (na,b,t) (i, subst) ->
+ if b == None then
+ let t = mkProj (ps.(i), mkRel 1) in
+ (i + 1, t :: subst)
+ else (i, mkRel 0 :: subst))
+ ctx (0, [])
+ in
+ let term = substl subst br in
+ term
+ in
+ it_mkLambda_or_LetIn_name env obj
(Termops.lift_rel_context nrec deparsign)
in