2 files changed, 10 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml
index fa21cd83ed..3b5c90b020 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -857,6 +857,13 @@ let rec prlist elem l = match l with
   | []   -> mt ()
   | h::t -> Stream.lapp (fun () -> elem h) (prlist elem t)
 
+(* unlike all other functions below, [prlist] works lazily.
+   if a strict behavior is needed, use [prlist_strict] instead. *)
+
+let rec prlist_strict elem l = match l with 
+  | []   -> mt ()
+  | h::t -> (elem h)++(prlist_strict elem t)
+
 let rec prlist_with_sep sep elem l = match l with
   | []   -> mt ()
   | [h]  -> elem h
diff --git a/lib/util.mli b/lib/util.mli
index 6d6d9c2a85..5e89788b9b 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -255,6 +255,9 @@ val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
 val nth : int -> std_ppcmds
 
 val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+(* unlike all other functions below, [prlist] works lazily.
+   if a strict behavior is needed, use [prlist_strict] instead. *)
+val prlist_strict :  ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 val prlist_with_sep :
    (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b list -> std_ppcmds
 val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds