module Wcclausenv

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@130 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 16 insertions, 5 deletions

diff --git a/lib/pp.mli b/lib/pp.mli
index c4600fcdf0..8906616ac4 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -51,7 +51,7 @@ val tB : 'a ppcmd_token
 val cLOSE : 'a ppcmd_token
 val tCLOSE : 'a ppcmd_token
 
-(*s Pretty-printing functions WITHOUT FLUSH. *)
+(*s Pretty-printing functions \emph{without flush}. *)
 
 val pP_with : Format.formatter -> std_ppcmds -> unit
 val pPNL_with : Format.formatter -> std_ppcmds -> unit
@@ -59,7 +59,7 @@ val warning_with : Format.formatter -> string -> unit
 val wARN_with : Format.formatter -> std_ppcmds -> unit
 val pp_flush_with : Format.formatter -> unit -> unit
 
-(*s Pretty-printing functions WITH FLUSH. *)
+(*s Pretty-printing functions \emph{with flush}. *)
 
 val mSG_with : Format.formatter -> std_ppcmds -> unit
 val mSGNL_with : Format.formatter -> std_ppcmds -> unit
@@ -68,7 +68,7 @@ val mSGNL_with : Format.formatter -> std_ppcmds -> unit
 (*s The following functions are instances of the previous ones on
   [std_ft] and [err_ft]. *)
 
-(*s Pretty-printing functions WITHOUT FLUSH on [stdout] and [stderr]. *)
+(*s Pretty-printing functions \emph{without flush} on [stdout] and [stderr]. *)
 
 val pP : std_ppcmds -> unit
 val pPNL : std_ppcmds -> unit
@@ -80,7 +80,7 @@ val wARN : std_ppcmds -> unit
 val pp_flush : unit -> unit
 val flush_all: unit -> unit
 
-(*s Pretty-printing functions WITH FLUSH on [stdout] and [stderr]. *)
+(*s Pretty-printing functions \emph{with flush} on [stdout] and [stderr]. *)
 
 val mSG : std_ppcmds -> unit
 val mSGNL : std_ppcmds -> unit
diff --git a/lib/util.ml b/lib/util.ml
index f3bc44ebf4..46474ad936 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -320,6 +320,12 @@ let intmap_to_list m = Intmap.fold (fun n v l -> (n,v)::l) m []
 
 let intmap_inv m b = Intmap.fold (fun n v l -> if v = b then n::l else l) m []
 
+let interval n m = 
+  let rec interval_n (l,m) =
+    if n > m then l else interval_n (m::l,pred m)
+  in 
+  interval_n ([],m)
+
 let in_some x = Some x
 
 let out_some = function
diff --git a/lib/util.mli b/lib/util.mli
index 4f992ffd4e..1952dc46cd 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -5,7 +5,10 @@
 open Pp
 (*i*)
 
-(* Errors. [Anomaly] is used for system errors and [UserError] for the
+(* This module contains numerous utility functions on strings, lists,
+   arrays, etc. *)
+
+(*s Errors. [Anomaly] is used for system errors and [UserError] for the
    user's ones. *)
 
 exception Anomaly of string * std_ppcmds
@@ -92,6 +95,8 @@ val intmap_in_dom : int -> 'a Intmap.t -> bool
 val intmap_to_list : 'a Intmap.t -> (int * 'a) list
 val intmap_inv : 'a Intmap.t -> 'a -> int list
 
+val interval : int -> int -> int list
+
 val in_some : 'a -> 'a option
 val out_some : 'a option -> 'a
 val option_app : ('a -> 'b) -> 'a option -> 'b option