From ccdc62a6b4722c38f2b37cbf21b14e5094255390 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 21 Jan 2016 18:05:55 -0500 Subject: Fix bug #4506. Using betadeltaiota_nolet might produce terms of the form (let x := t in u) a that should be reduced. Maybe a different decomposition/reduction primitive should be used instead. --- pretyping/indrec.ml | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'pretyping/indrec.ml') diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index d5f6e9b30..0588dcc87 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -155,7 +155,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = | Prod (n,t,c) -> let d = (n,None,t) in make_prod env (n,t,prec (push_rel d env) (i+1) (d::sign) c) - | LetIn (n,b,t,c) -> + | LetIn (n,b,t,c) when List.is_empty largs -> let d = (n,Some b,t) in mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::sign) c) | Ind (_,_) -> @@ -166,7 +166,10 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = base [|applist (mkRel (i+1), Termops.extended_rel_list 0 sign)|] else base - | _ -> assert false + | _ -> + let t' = whd_betadeltaiota env sigma p in + if Term.eq_constr p' t' then assert false + else prec env i sign t' in prec env 0 [] in @@ -230,14 +233,17 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = | Prod (n,t,c) -> let d = (n,None,t) in mkLambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c) - | LetIn (n,b,t,c) -> + | LetIn (n,b,t,c) when List.is_empty largs -> let d = (n,Some b,t) in mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c) | Ind _ -> let realargs = List.skipn nparrec largs and arg = appvect (mkRel (i+1), Termops.extended_rel_vect 0 hyps) in applist(lift i fk,realargs@[arg]) - | _ -> assert false + | _ -> + let t' = whd_betadeltaiota env sigma p in + if Term.eq_constr t' p' then assert false + else prec env i hyps t' in prec env 0 [] in -- cgit v1.2.3