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 /kernel/modops.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 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 5eddb6c843..19075058a6 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -562,7 +562,7 @@ and clean_expr l = function if str_clean == str && sig_clean = sigt.typ_expr then s else SEBfunctor (mbid,{sigt with typ_expr=sig_clean},str_clean) | SEBstruct str as s-> - let str_clean = Util.list_smartmap (clean_struct l) str in + let str_clean = Util.List.smartmap (clean_struct l) str in if str_clean == str then s else SEBstruct(str_clean) | str -> str @@ -572,7 +572,7 @@ let rec collect_mbid l = function if str_clean == str then s else SEBfunctor (mbid,sigt,str_clean) | SEBstruct str as s-> - let str_clean = Util.list_smartmap (clean_struct l) str in + let str_clean = Util.List.smartmap (clean_struct l) str in if str_clean == str then s else SEBstruct(str_clean) | _ -> anomaly "Modops:the evaluation of the structure failed " |