aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/util.ml
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-15 18:59:07 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-15 18:59:07 +0000
commit566e21af6792406715e79df5c61a3cc715b15c66 (patch)
tree5bd0a8c88f110e6fbfe2b2d25778fd3a01e0a833 /lib/util.ml
parent77ba6079eef1099a34bfcff01fe36298392e3fdf (diff)
Document Generalizable Variables, and change syntax to
[Generalizable (All|No) Variables (ident+)?], also update type classes documentation to reflect the latest changes in instance decls. Fix a bug in [Util.list_split_when]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12525 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/util.ml')
-rw-r--r--lib/util.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/util.ml b/lib/util.ml
index 9f29d55bd..5e2a071a9 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -810,7 +810,7 @@ let list_split_at index l =
let list_split_when p =
let rec split_when_loop x y =
match y with
- | [] -> ([],[])
+ | [] -> (List.rev x,[])
| (a::l) -> if (p a) then (List.rev x,y) else split_when_loop (a::x) l
in
split_when_loop []