From f8394a52346bf1e6f98e7161e75fb65bd0631391 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 14 Sep 2012 16:17:09 +0000 Subject: Moving Utils.list_* to a proper CList module, which includes stdlib List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/heads.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'library/heads.ml') diff --git a/library/heads.ml b/library/heads.ml index c86a91cc9..f3bcba770 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -113,8 +113,8 @@ let kind_of_head env t = k+n-m,[],a else (* enough arguments to [cst] *) - k,list_skipn n l,List.nth l (i-1) in - let l' = list_tabulate (fun _ -> mkMeta 0) q @ rest in + k,List.skipn n l,List.nth l (i-1) in + let l' = List.tabulate (fun _ -> mkMeta 0) q @ rest in aux k' l' a (with_subcase or with_case) | ConstructorHead when with_case -> NotImmediatelyComputableHead | x -> x -- cgit v1.2.3