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 /printing/ppconstr.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 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index f99d8c109f..190181c23f 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -460,8 +460,8 @@ let pr pr sep inherited a = pr spc ltop b), lletin | CAppExpl (_,(Some i,f),l) -> - let l1,l2 = list_chop i l in - let c,l1 = list_sep_last l1 in + let l1,l2 = List.chop i l in + let c,l1 = List.sep_last l1 in let p = pr_proj (pr mt) pr_appexpl c f l1 in if l2<>[] then p ++ prlist (pr spc (lapp,L)) l2, lapp @@ -473,8 +473,8 @@ let pr pr sep inherited a = hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), larg | CAppExpl (_,(None,f),l) -> pr_appexpl (pr mt) f l, lapp | CApp (_,(Some i,f),l) -> - let l1,l2 = list_chop i l in - let c,l1 = list_sep_last l1 in + let l1,l2 = List.chop i l in + let c,l1 = List.sep_last l1 in assert (snd c = None); let p = pr_proj (pr mt) pr_app (fst c) f l1 in if l2<>[] then |