diff options
Diffstat (limited to 'kernel/closure.mli')
| -rw-r--r-- | kernel/closure.mli | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/kernel/closure.mli b/kernel/closure.mli index 924da0a5..c814baad 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: closure.mli 9215 2006-10-05 15:40:31Z herbelin $ i*) +(*i $Id: closure.mli 10652 2008-03-10 21:52:06Z herbelin $ i*) (*i*) open Pp @@ -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 @@ -80,6 +76,7 @@ val betadeltaiota : reds val betaiotazeta : reds val betadeltaiotanolet : reds +val unfold_side_red : reds val unfold_red : evaluable_global_reference -> reds (***********************************************************************) |