diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-20 19:46:56 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-20 19:46:56 +0000 |
| commit | 30cc204e35e6ff422396b85d3b649d38f6a97c1e (patch) | |
| tree | 53788685c3808ad12a96ee530f2533d820124b73 /kernel | |
| parent | b9da9226ebd8a2db21570ba269663e16f63e1815 (diff) | |
Bug mauvais environnement dans le test d'eta-conversion
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1170 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/reduction.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index a5f9114a8..4df8de1a2 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -267,7 +267,7 @@ let reduce_fix whdfun fix stack = (* Generic reduction function *) -let whd_state_gen flags env sigma = +let rec whd_state_gen flags env sigma = let rec whrec (x, stack as s) = match kind_of_term x with | IsRel n when red_delta flags -> @@ -289,15 +289,17 @@ let whd_state_gen flags env sigma = | IsLetIn (_,b,_,c) when red_letin flags -> stacklam whrec [b] c stack | IsCast (c,_) -> whrec (c, stack) | IsApp (f,cl) -> whrec (f, append_stack cl stack) - | IsLambda (_,_,c) -> + | IsLambda (na,t,c) -> (match decomp_stack stack with | Some (a,m) when red_beta flags -> stacklam whrec [a] c m | None when red_eta flags -> - (match kind_of_term (app_stack (whrec (c, empty_stack))) with + let env' = push_rel_assum (na,t) env in + let whrec' = whd_state_gen flags env' sigma in + (match kind_of_term (app_stack (whrec' (c, empty_stack))) with | IsApp (f,cl) -> let napp = Array.length cl in if napp > 0 then - let x', l' = whrec (array_last cl, empty_stack) in + let x', l' = whrec' (array_last cl, empty_stack) in match kind_of_term x', decomp_stack l' with | IsRel 1, None -> let lc = Array.sub cl 0 (napp-1) in |