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 /kernel/declarations.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/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 5f677d056..a2ce4f270 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -110,7 +110,7 @@ let subst_rel_declaration sub (id,copt,t as x) = let t' = subst_mps sub t in if copt == copt' & t == t' then x else (id,copt',t') -let subst_rel_context sub = list_smartmap (subst_rel_declaration sub) +let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) (* TODO: these substitution functions could avoid duplicating things when the substitution have preserved all the fields *) @@ -141,11 +141,11 @@ let hcons_rel_decl ((n,oc,t) as d) = and t' = hcons_types t in if n' == n && oc' == oc && t' == t then d else (n',oc',t') -let hcons_rel_context l = list_smartmap hcons_rel_decl l +let hcons_rel_context l = List.smartmap hcons_rel_decl l let hcons_polyarity ar = { poly_param_levels = - list_smartmap (Option.smartmap hcons_univ) ar.poly_param_levels; + List.smartmap (Option.smartmap hcons_univ) ar.poly_param_levels; poly_level = hcons_univ ar.poly_level } let hcons_const_type = function |