diff options
| author | herbelin | 2003-01-15 15:33:11 +0000 |
|---|---|---|
| committer | herbelin | 2003-01-15 15:33:11 +0000 |
| commit | d72eb6e333f710bb8f4ea0061e8399aafba19fe0 (patch) | |
| tree | a6886d7a87a3d1614adcfdfb641ea859f488fc9c | |
| parent | a6ce286c10edf79a57c69acffc67fcd254b88d36 (diff) | |
Bug en présence de let-in
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3498 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/indrec.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index f508ac886b..ed549a77ed 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -151,13 +151,13 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = (nhyps-1) (i::li)) | Some(dep',p) -> let nP = lift (i+1+decP) p in - let t_0 = process_pos env dep' nP (lift 1 t) in + let env' = push_rel (n,None,t) env in + let t_0 = process_pos env' dep' nP (lift 1 t) in make_prod_dep (dep or dep') env (n,t, mkArrow t_0 (process_constr - (push_rel (n,None,t) - (push_rel (Anonymous,None,t_0) env)) + (push_rel (Anonymous,None,t_0) env') (i+2) (lift 1 c_0) rest (nhyps-1) (i::li)))) | LetIn (n,b,t,c_0) -> mkLetIn (n,b,t, @@ -217,9 +217,10 @@ let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs = (cprest,rest)) | Some(_,f_0) -> let nF = lift (i+1+decF) f_0 in - let arg = process_pos env nF (lift 1 t) in + let env' = push_rel d env in + let arg = process_pos env' nF (lift 1 t) in lambda_name env - (n,t,process_constr (push_rel d env) (i+1) + (n,t,process_constr env' (i+1) (whd_beta (applist (lift 1 f, [(mkRel 1); arg]))) (cprest,rest))) | (n,Some c,t as d)::cprest, rest -> |