diff options
Diffstat (limited to 'kernel/closure.mli')
| -rw-r--r-- | kernel/closure.mli | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/kernel/closure.mli b/kernel/closure.mli index 2a0c1f89e..ea8bccede 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -37,11 +37,7 @@ module type RedFlagsSig = sig type reds type red_kind - (* The different kind of reduction *) - (* Const/Var means the reference as argument should be unfolded *) - (* Constbut/Varbut means all references except the ones as argument - of Constbut/Varbut should be unfolded (there may be several such - Constbut/Varbut *) + (* The different kinds of reduction *) val fBETA : red_kind val fDELTA : red_kind val fIOTA : red_kind |