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/extract_env.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/extract_env.ml')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 588fe0cf23..b5cdec3ece 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -150,9 +150,9 @@ let factor_fix env l cb msb = if n = 1 then [|l|], recd, msb else begin if List.length msb < n-1 then raise Impossible; - let msb', msb'' = list_chop (n-1) msb in + let msb', msb'' = List.chop (n-1) msb in let labels = Array.make n l in - list_iter_i + List.iter_i (fun j -> function | (l,SFBconst cb') -> @@ -207,7 +207,7 @@ let env_for_mtb_with_def env mp seb idl = in let l = label_of_id (List.hd idl) in let spot = function (l',SFBconst _) -> l = l' | _ -> false in - let before = fst (list_split_when spot sig_b) in + let before = fst (List.split_when spot sig_b) in Modops.add_signature mp before empty_delta_resolver env (* From a [structure_body] (i.e. a list of [structure_field_body]) |