diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-14 16:17:09 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-14 16:17:09 +0000 |
| commit | f8394a52346bf1e6f98e7161e75fb65bd0631391 (patch) | |
| tree | ae133cc5207283e8c5a89bb860435b37cbf6ecdb /checker/closure.ml | |
| parent | 6dae53d279afe2b8dcfc43dd2aded9431944c5c8 (diff) | |
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
Diffstat (limited to 'checker/closure.ml')
| -rw-r--r-- | checker/closure.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/closure.ml b/checker/closure.ml index 7f23ed201..c3351cea1 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -370,7 +370,7 @@ let rec compact_constr (lg, subs as s) c k = match c with Rel i -> if i < k then c,s else - (try Rel (k + lg - list_index (i-k+1) subs), (lg,subs) + (try Rel (k + lg - List.index (i-k+1) subs), (lg,subs) with Not_found -> Rel (k+lg), (lg+1, (i-k+1)::subs)) | (Sort _|Var _|Meta _|Ind _|Const _|Construct _) -> c,s | Evar(ev,v) -> @@ -648,7 +648,7 @@ let rec get_args n tys f e stk = let eargs = Array.sub l n (na-n) in (Inl (subs_cons(args,e)), Zapp eargs :: s) else (* more lambdas *) - let etys = list_skipn na tys in + let etys = List.skipn na tys in get_args (n-na) etys f (subs_cons(l,e)) s | _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk) |