diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-01-21 18:05:55 -0500 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-01-23 15:58:05 -0500 |
| commit | ccdc62a6b4722c38f2b37cbf21b14e5094255390 (patch) | |
| tree | 9dea2af3a7c398cd66a0abd60d6bec6094951ffe /pretyping/indrec.ml | |
| parent | f65f8d5a4d9ba437fa2d8af03e2781d841e53007 (diff) | |
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.
Diffstat (limited to 'pretyping/indrec.ml')
| -rw-r--r-- | pretyping/indrec.ml | 14 |
1 files changed, 10 insertions, 4 deletions
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 |