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 /plugins/extraction/common.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/common.ml')
| -rw-r--r-- | plugins/extraction/common.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index b6b7e5833..8cceb2a11 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -349,7 +349,7 @@ let rec mp_renaming_fun mp = match mp with | MPfile _ -> assert (modular ()); (* see [at_toplevel] above *) assert (get_phase () = Pre); - let current_mpfile = (list_last (get_visible ())).mp in + let current_mpfile = (List.last (get_visible ())).mp in if mp <> current_mpfile then mpfiles_add mp; [string_of_modfile mp] @@ -496,7 +496,7 @@ let fstlev_ks k = function let pp_ocaml_local k prefix mp rls olab = (* what is the largest prefix of [mp] that belongs to [visible]? *) assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *) - let rls' = list_skipn (mp_length prefix) rls in + let rls' = List.skipn (mp_length prefix) rls in let k's = fstlev_ks k rls' in (* Reference r / module path mp is of the form [<prefix>.s.<...>]. *) if not (visible_clash prefix k's) then dottify rls' |