From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 kernel/closure.mli | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

(limited to 'kernel/closure.mli')

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
 
 (***********************************************************************)
-- 
cgit v1.2.3