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.ml  | 9 +++++++++
 lib/util.mli | 2 ++
 2 files changed, 11 insertions(+)

(limited to 'lib')

diff --git a/lib/util.ml b/lib/util.ml
index a8e716e0f3..242c203211 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -1000,6 +1000,15 @@ let array_fold_left2_i f a v1 v2 =
   if Array.length v2 <> lv1 then invalid_arg "array_fold_left2";
   fold a 0
 
+let array_fold_left3 f a v1 v2 v3 =
+  let lv1 = Array.length v1 in
+  let rec fold a n =
+    if n >= lv1 then a else fold (f a v1.(n) v2.(n) v3.(n)) (succ n)
+  in
+  if Array.length v2 <> lv1 || Array.length v3 <> lv1 then
+    invalid_arg "array_fold_left2";
+  fold a 0
+
 let array_fold_left_from n f a v =
   let rec fold a n =
     if n >= Array.length v then a else fold (f a v.(n)) (succ n)
diff --git a/lib/util.mli b/lib/util.mli
index 5248d0e6b1..2216ba9813 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