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 /pretyping/pretyping.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 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 5113236954..0eff92b617 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -79,7 +79,7 @@ let search_guard loc env possible_indexes fixdefs = let fix = ((indexes, 0),fixdefs) in try check_fix env fix; raise (Found indexes) with TypeError _ -> ()) - (list_combinations possible_indexes); + (List.combinations possible_indexes); let errmsg = "Cannot guess decreasing argument of fix." in if loc = Loc.ghost then error errmsg else user_err_loc (loc,"search_guard", Pp.str errmsg) @@ -363,7 +363,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function Array.to_list (Array.mapi (fun i (n,_) -> match n with | Some n -> [n] - | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i)) + | None -> List.map_i (fun i _ -> i) 0 ctxtv.(i)) vn) in let fixdecls = (names,ftys,fdefs) in |