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 /interp/coqlib.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 'interp/coqlib.ml')
| -rw-r--r-- | interp/coqlib.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 94cb917497..531ca5bf45 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -45,7 +45,7 @@ let gen_constant_in_modules locstr dirs s = let dirs = List.map make_dir dirs in let qualid = qualid_of_string s in let all = Nametab.locate_extended_all qualid in - let all = list_uniquize (list_map_filter global_of_extended all) in + let all = List.uniquize (List.map_filter global_of_extended all) in let these = List.filter (has_suffix_in_dirs dirs) all in match these with | [x] -> constr_of_global x @@ -73,7 +73,7 @@ let check_required_library d = if not (Library.library_is_loaded dir) then if not current_dir then (* Loading silently ... - let m, prefix = list_sep_last d' in + let m, prefix = List.sep_last d' in read_library (Loc.ghost,make_qualid (make_dirpath (List.rev prefix)) m) *) |