diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/closure.ml | 9 | ||||
| -rw-r--r-- | kernel/closure.mli | 1 |
2 files changed, 7 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] *) diff --git a/kernel/closure.mli b/kernel/closure.mli index ea8bccede8..926e152e04 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -76,6 +76,7 @@ val betadeltaiota : reds val betaiotazeta : reds val betadeltaiotanolet : reds +val unfold_side_red : reds val unfold_red : evaluable_global_reference -> reds (***********************************************************************) |