Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg

40 files changed, 86 insertions, 46 deletions

diff --git a/lib/bigint.ml b/lib/bigint.ml
index 084189a8..b33baa83 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: bigint.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (*i*)
 open Pp
diff --git a/lib/bigint.mli b/lib/bigint.mli
index 01bfedac..48e36875 100644
--- a/lib/bigint.mli
+++ b/lib/bigint.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: bigint.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/lib/bstack.ml b/lib/bstack.ml
index 6330afec..4afbe41e 100644
--- a/lib/bstack.ml
+++ b/lib/bstack.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: bstack.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (* Queues of a given length *)
 
diff --git a/lib/bstack.mli b/lib/bstack.mli
index 057bace3..b34d18d7 100644
--- a/lib/bstack.mli
+++ b/lib/bstack.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: bstack.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* Bounded stacks. If the depth is [None], then there is no depth limit. *)
 
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 09c9a38c..8a2a467a 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: dyn.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 
diff --git a/lib/dyn.mli b/lib/dyn.mli
index 290907b1..512baf7f 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: dyn.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* Dynamics. Use with extreme care. Not for kids. *)
 
diff --git a/lib/edit.ml b/lib/edit.ml
index 18d8d8dc..edfde186 100644
--- a/lib/edit.ml
+++ b/lib/edit.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: edit.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/lib/edit.mli b/lib/edit.mli
index 4274846e..3d6f98ab 100644
--- a/lib/edit.mli
+++ b/lib/edit.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: edit.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* The type of editors.
  * An editor is a finite map, ['a -> 'b], which knows how to apply
diff --git a/lib/explore.ml b/lib/explore.ml
index c20726aa..c6a40e04 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: explore.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Format
 
diff --git a/lib/explore.mli b/lib/explore.mli
index b7fe7a5a..f8180577 100644
--- a/lib/explore.mli
+++ b/lib/explore.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: explore.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*s Search strategies. *)
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 2961d83f..de70b6a6 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: flags.ml 13358 2010-07-29 23:10:17Z herbelin $ i*)
 
 let with_option o f x =
   let old = !o in o:=true;
@@ -35,8 +35,6 @@ let dont_load_proofs = ref false
 
 let raw_print = ref false
 
-let unicode_syntax = ref false
-
 (* Compatibility mode *)
 
 type compat_version = V8_2
diff --git a/lib/flags.mli b/lib/flags.mli
index 87c8e792..75cfc96d 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: flags.mli 13358 2010-07-29 23:10:17Z herbelin $ i*)
 
 (* Global options of the system. *)
 
@@ -27,8 +27,6 @@ val dont_load_proofs : bool ref
 
 val raw_print : bool ref
 
-val unicode_syntax : bool ref
-
 type compat_version = V8_2
 val compat_version : compat_version option ref
 val version_strictly_greater : compat_version -> bool
diff --git a/lib/gmap.ml b/lib/gmap.ml
index 41a57276..1544dacc 100644
--- a/lib/gmap.ml
+++ b/lib/gmap.ml
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id$ *)
+(* $Id: gmap.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (* Maps using the generic comparison function of ocaml. Code borrowed from
    the ocaml standard library (Copyright 1996, INRIA). *)
diff --git a/lib/gmap.mli b/lib/gmap.mli
index 3e125a60..379aa63f 100644
--- a/lib/gmap.mli
+++ b/lib/gmap.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: gmap.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* Maps using the generic comparison function of ocaml. Same interface as
    the module [Map] from the ocaml standard library. *)
diff --git a/lib/gmapl.ml b/lib/gmapl.ml
index 87804bb5..5f539971 100644
--- a/lib/gmapl.ml
+++ b/lib/gmapl.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: gmapl.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 
diff --git a/lib/gmapl.mli b/lib/gmapl.mli
index 95a80a29..7c5d0ceb 100644
--- a/lib/gmapl.mli
+++ b/lib/gmapl.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: gmapl.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* Maps from ['a] to lists of ['b]. *)
 
diff --git a/lib/gset.ml b/lib/gset.ml
index fca46496..dc88127e 100644
--- a/lib/gset.ml
+++ b/lib/gset.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: gset.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (* Sets using the generic comparison function of ocaml. Code borrowed from
    the ocaml standard library. *)
diff --git a/lib/gset.mli b/lib/gset.mli
index 570ce5e0..911ff3f0 100644
--- a/lib/gset.mli
+++ b/lib/gset.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: gset.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* Sets using the generic comparison function of ocaml. Same interface as
    the module [Set] from the ocaml standard library. *)
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index 6841132e..1ebf8773 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: hashcons.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (* Hash consing of datastructures *)
 
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index 3fbf3c9b..0ce4d3b9 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: hashcons.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* Generic hash-consing. *)
 
diff --git a/lib/heap.ml b/lib/heap.ml
index 5f70b5f2..47cfb46f 100644
--- a/lib/heap.ml
+++ b/lib/heap.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: heap.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (*s Heaps *)
 
diff --git a/lib/heap.mli b/lib/heap.mli
index edafef5d..e46f97ac 100644
--- a/lib/heap.mli
+++ b/lib/heap.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: heap.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* Heaps *)
 
diff --git a/lib/option.ml b/lib/option.ml
index e5b9ecd3..850d7306 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: option.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (** Module implementing basic combinators for OCaml option type.
    It tries follow closely the style of OCaml standard library.
diff --git a/lib/option.mli b/lib/option.mli
index 03e989d3..c76deb3c 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: option.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (** Module implementing basic combinators for OCaml option type.
    It tries follow closely the style of OCaml standard library.
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 0983e5e7..87c12fba 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: pp.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp_control
 
diff --git a/lib/pp.mli b/lib/pp.mli
index 03aa1f9c..4b8e5a29 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: pp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Pp_control
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
index 54e8fa0c..507a54a7 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: pp_control.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (* Parameters of pretty-printing *)
 
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
index c1540e72..bf95bb5e 100644
--- a/lib/pp_control.mli
+++ b/lib/pp_control.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: pp_control.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* Parameters of pretty-printing. *)
 
diff --git a/lib/predicate.ml b/lib/predicate.ml
index af66c0f2..506a87c9 100644
--- a/lib/predicate.ml
+++ b/lib/predicate.ml
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: predicate.ml 12337 2009-09-17 15:58:14Z glondu $ *)
 
 (* Sets over ordered types *)
 
diff --git a/lib/predicate.mli b/lib/predicate.mli
index 41d5399b..85596fea 100644
--- a/lib/predicate.mli
+++ b/lib/predicate.mli
@@ -1,5 +1,5 @@
 
-(*i $Id$ i*)
+(*i $Id: predicate.mli 6621 2005-01-21 17:24:37Z herbelin $ i*)
 
 (* Module [Pred]: sets over infinite ordered types with complement. *)
 
diff --git a/lib/profile.ml b/lib/profile.ml
index b612f31d..87bfe624 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: profile.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Gc
 
diff --git a/lib/profile.mli b/lib/profile.mli
index bde8587c..e61aba85 100644
--- a/lib/profile.mli
+++ b/lib/profile.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: profile.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*s This program is a small time and allocation profiler for Objective Caml *)
 
diff --git a/lib/rtree.ml b/lib/rtree.ml
index 55b00a93..a7428e12 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: rtree.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Util
 
diff --git a/lib/rtree.mli b/lib/rtree.mli
index 3013199a..17cccfc8 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: rtree.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* Type of regular tree with nodes labelled by values of type 'a *)
 (* The implementation uses de Bruijn indices, so binding capture
diff --git a/lib/system.ml b/lib/system.ml
index 7e7dfbcb..17d211f8 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: system.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/lib/system.mli b/lib/system.mli
index 44314c23..971a5c86 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: system.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*s Files and load paths. Load path entries remember the original root
     given by the user. For efficiency, we keep the full path (field
diff --git a/lib/tlm.ml b/lib/tlm.ml
index 098a1247..aad4d363 100644
--- a/lib/tlm.ml
+++ b/lib/tlm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: tlm.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 type ('a,'b) t = Node of 'b Gset.t * ('a, ('a,'b) t) Gmap.t
 
diff --git a/lib/tlm.mli b/lib/tlm.mli
index 95a788ff..db3d7dd3 100644
--- a/lib/tlm.mli
+++ b/lib/tlm.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: tlm.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* Tries. This module implements a data structure [('a,'b) t] mapping lists
    of values of type ['a] to sets (as lists) of values of type ['b]. *)
diff --git a/lib/util.ml b/lib/util.ml
index 6d04c3c2..851afc60 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(* $Id: util.ml 13357 2010-07-29 22:59:55Z herbelin $ *)
 
 open Pp
 
@@ -43,6 +43,7 @@ let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s)
 
 let located_fold_left f x (_,a) = f x a
 let located_iter2 f (_,a) (_,b) = f a b
+let down_located f (_,a) = f a
 
 (* Like Exc_located, but specifies the outermost file read, the filename
    associated to the location of the error, and the error itself. *)
@@ -66,6 +67,11 @@ let pi1 (a,_,_) = a
 let pi2 (_,a,_) = a
 let pi3 (_,_,a) = a
 
+(* Projection operator *)
+
+let down_fst f x = f (fst x)
+let down_snd f x = f (snd x)
+
 (* Characters *)
 
 let is_letter c = (c >= 'a' && c <= 'z') or (c >= 'A' && c <= 'Z')
@@ -700,6 +706,16 @@ let list_split_when p =
   in
   split_when_loop []
 
+(* [list_split_by p l] splits [l] into two lists [(l1,l2)] such that elements of
+   [l1] satisfy [p] and elements of [l2] do not *)
+let list_split_by p =
+  let rec split_by_loop = function
+  | []   -> ([],[])
+  | a::l ->
+      let (l1,l2) = split_by_loop l in if p a then (a::l1,l2) else (l1,a::l2)
+  in
+  split_by_loop
+
 let rec list_split3 = function
   | [] -> ([], [], [])
   | (x,y,z)::l ->
@@ -828,6 +844,13 @@ let list_cartesians op init ll =
 
 let list_combinations l = list_cartesians (fun x l -> x::l) [] l
 
+let rec list_combine3 x y z = 
+  match x, y, z with
+  | [], [], [] -> []
+  | (x :: xs), (y :: ys), (z :: zs) ->
+      (x, y, z) :: list_combine3 xs ys zs
+  | _, _, _ -> raise (Invalid_argument "list_combine3")
+  
 (* Keep only those products that do not return None *)
 
 let rec list_cartesian_filter op l1 l2 =
@@ -1171,6 +1194,12 @@ let iterate_for a b f x =
   let rec iterate i v = if i > b then v else iterate (succ i) (f i v) in
   iterate a x
 
+(* Delayed computations *)
+
+type 'a delayed = unit -> 'a
+
+let delayed_force f = f ()
+
 (* Misc *)
 
 type ('a,'b) union = Inl of 'a | Inr of 'b
diff --git a/lib/util.mli b/lib/util.mli
index cd8e3135..00c73a1f 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: util.mli 13357 2010-07-29 22:59:55Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -52,6 +52,7 @@ val invalid_arg_loc : loc * string -> 'a
 val join_loc : loc -> loc -> loc
 val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
 val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
+val down_located : ('a -> 'b) -> 'a located -> 'b
 
 (* Like [Exc_located], but specifies the outermost file read, the
    input buffer associated to the location of the error (or the module name
@@ -64,6 +65,11 @@ exception Error_in_file of string * (bool * string * loc) * exn
 val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
 val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
 
+(* Going down pairs *)
+
+val down_fst : ('a -> 'b) -> 'a * 'c -> 'b
+val down_snd : ('a -> 'b) -> 'c * 'a -> 'b
+
 (* Mapping under triple *)
 
 val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd
@@ -170,6 +176,7 @@ val list_merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
 val list_subset : 'a list -> 'a list -> bool
 val list_split_at : int -> 'a list -> 'a list*'a list
 val list_split_when : ('a -> bool) -> 'a list -> 'a list * 'a list
+val list_split_by : ('a -> bool) -> 'a list -> 'a list * 'a list
 val list_split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
 val list_partition_by : ('a -> 'a -> bool) -> 'a list -> 'a list list
 val list_firstn : int -> 'a list -> 'a list
@@ -202,7 +209,9 @@ val list_cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
 val list_cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
 (* list_combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
 val list_combinations : 'a list list -> 'a list list
-(* Keep only those products that do not return None *)
+val list_combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
+
+(** Keep only those products that do not return None *)
 val list_cartesian_filter :
   ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
 val list_cartesians_filter :
@@ -272,7 +281,13 @@ val iterate : ('a -> 'a) -> int -> 'a -> 'a
 val repeat : int -> ('a -> unit) -> 'a -> unit
 val iterate_for : int -> int -> (int -> 'a -> 'a) -> 'a -> 'a
 
-(*s Misc. *)
+(** {6 Delayed computations. } *)
+
+type 'a delayed = unit -> 'a
+
+val delayed_force : 'a delayed -> 'a
+
+(** {6 Misc. } *)
 
 type ('a,'b) union = Inl of 'a | Inr of 'b