diff options
Diffstat (limited to 'kernel/closure.ml')
| -rw-r--r-- | kernel/closure.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 01d31441d6..2ee2443ffc 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -165,12 +165,15 @@ let betadeltaiotanolet = mkflags [fBETA;fDELTA;fIOTA] let betaiota = mkflags [fBETA;fIOTA] let beta = mkflags [fBETA] let betaiotazeta = mkflags [fBETA;fIOTA;fZETA] + +(* Removing fZETA for finer behaviour would break many developments *) +let unfold_side_flags = [fBETA;fIOTA;fZETA] +let unfold_side_red = mkflags [fBETA;fIOTA;fZETA] let unfold_red kn = let flag = match kn with | EvalVarRef id -> fVAR id - | EvalConstRef kn -> fCONST kn - in (* Remove fZETA for finer behaviour ? *) - mkflags [fBETA;flag;fIOTA;fZETA] + | EvalConstRef kn -> fCONST kn in + mkflags (flag::unfold_side_flags) (************************* Obsolète (* [r_const=(true,cl)] means all constants but those in [cl] *) |