diff options
| author | ppedrot | 2012-09-14 16:17:09 +0000 |
|---|---|---|
| committer | ppedrot | 2012-09-14 16:17:09 +0000 |
| commit | f8394a52346bf1e6f98e7161e75fb65bd0631391 (patch) | |
| tree | ae133cc5207283e8c5a89bb860435b37cbf6ecdb /plugins/extraction/modutil.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 'plugins/extraction/modutil.ml')
| -rw-r--r-- | plugins/extraction/modutil.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 1211bbf173..8659de03eb 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -30,7 +30,7 @@ let se_iter do_decl do_spec = | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt' | MTwith (mt,ML_With_type(idl,l,t))-> let mp_mt = msid_of_mt mt in - let l',idl' = list_sep_last idl in + let l',idl' = List.sep_last idl in let mp_w = List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl' in |