]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/extlib/hExtlib.mli
Final implementation of proof irrelevant conversion, which hadn't
[helm.git] / helm / software / components / extlib / hExtlib.mli
index c80d2e4f85f2a5b3bc2a33b009be934eeecd4a38..dae91447741280aa05331a4ab49d44822048392f 100644 (file)
@@ -100,7 +100,9 @@ val list_iter_default2: ('a -> 'b -> unit) -> 'a list -> 'b -> 'b list -> unit
    length (otherwise it raises Invalid_argument). It stops when the first two
    lists are empty. The third one can be shorter and is padded with a default value. *)
 val list_forall_default3: ('a -> 'b -> 'c -> bool) -> 'a list -> 'b list -> 'c -> 'c list -> bool
+val list_forall_default3_var: ('a -> 'b -> 'c -> bool) -> 'a list -> 'b list -> 'c -> 'c list -> bool
 
+exception FailureAt of int
 
   (** split_nth n l
    * @returns two list, the first contains at least n elements, the second the