From 0c2dd4a32538ebda7c964c249f158054b6cc2e1a Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 5 Mar 2011 16:42:38 +0000 Subject: Starting being more explicit on the reasons why module subtyping fails. Note: I'm unsure about some subtyping error case apparently involving aliases of inductive types (middle of Subtyping.check_inductive); I bound it to some NotEqualInductiveAliases error, but this has to be checked. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13885 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/util.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'lib/util.mli') diff --git a/lib/util.mli b/lib/util.mli index 5248d0e6b..2216ba981 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -259,6 +259,8 @@ val array_fold_right2 : ('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c val array_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a +val array_fold_left3 : + ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'a val array_fold_left2_i : (int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a val array_fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a -- cgit v1.2.3