From ff03e8dd0de507be82e58ed5e8fd902dfd7caf4b Mon Sep 17 00:00:00 2001 From: msozeau Date: Fri, 4 Jul 2008 14:38:44 +0000 Subject: Fixes in handling of implicit arguments: - Now [ id : Class foo ] makes id an explicit argument, and [ Class foo ] is equivalent to [ {someid} : Class foo ]. This makes declarations such as "Class Ord [ eq : Eq a ]" have sensible implicit args. - Better handling of {} in class and record declarations, refactorize code for declaring structures and classes. - Fix merging of implicit arguments information on section closing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11204 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/util.ml | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'lib/util.ml') diff --git a/lib/util.ml b/lib/util.ml index 14a40e378b..ebade654ef 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -576,6 +576,12 @@ let list_fold_left_i f = in it_list_f +let rec list_fold_left3 f accu l1 l2 l3 = + match (l1, l2, l3) with + ([], [], []) -> accu + | (a1::l1, a2::l2, a3::l3) -> list_fold_left3 f (f accu a1 a2 a3) l1 l2 l3 + | (_, _, _) -> invalid_arg "list_fold_left3" + (* [list_fold_right_and_left f [a1;...;an] hd = f (f (... (f (f hd an -- cgit v1.2.3