diff options
author | 2000-11-27 12:53:50 +0000 | |
---|---|---|
committer | 2000-11-27 12:53:50 +0000 | |
commit | 90ee69623ad22c122d76a8faf6127b96b8066a1c (patch) | |
tree | d45e62bad3904c8589cdd0cca8a409c6610fa0cc /kernel | |
parent | 500fb40a37455123d888cc6a2b595319dcbe8d67 (diff) |
Faut-il mettre la réduction let-in dans la réduction unfold ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@991 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/closure.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 004b59b10..b64f6fe59 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -77,7 +77,7 @@ let betaiotazeta_red = { let unfold_red sp = { r_beta = true; r_const = false,[sp]; - r_zeta = false; + r_zeta = true; (* false for finer behaviour ? *) r_evar = false; r_iota = true } |