diff options
| author | barras | 2007-07-12 17:15:22 +0000 |
|---|---|---|
| committer | barras | 2007-07-12 17:15:22 +0000 |
| commit | cae62c87e2a361aeb31d3382280e5d7f18126e92 (patch) | |
| tree | 4bca5f02028b68e98db4e34127f1e738dbc6d5b9 /kernel | |
| parent | bb3218e21e82cadacc2e22d9b55e3033df1744bb (diff) | |
normalisation (by closure) was not performed under fixpoints
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9983 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/closure.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 364475019f..01d31441d6 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -980,7 +980,7 @@ and knht e t stk = (************************************************************************) -(* Computes a normal form from the result of knh. *) +(* Computes a weak head normal form from the result of knh. *) let rec knr info m stk = match m.term with | FLambda(n,tys,f,e) when red_set info.i_flags fBETA -> @@ -1082,6 +1082,11 @@ and norm_head info m = let fbds = Array.map (mk_clos (subs_liftn (Array.length na) e)) bds in mkCoFix(n,(na, Array.map (kl info) ftys, Array.map (kl info) fbds)) + | FFix((n,(na,tys,bds)),e) -> + let ftys = Array.map (mk_clos e) tys in + let fbds = + Array.map (mk_clos (subs_liftn (Array.length na) e)) bds in + mkFix(n,(na, Array.map (kl info) ftys, Array.map (kl info) fbds)) | FEvar(i,args) -> mkEvar(i, Array.map (kl info) args) | t -> term_of_fconstr m |