From f8394a52346bf1e6f98e7161e75fb65bd0631391 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 14 Sep 2012 16:17:09 +0000
Subject: 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
---
 printing/printer.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 70a90b8ea6..1ad9dba499 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -289,7 +289,7 @@ let pr_concl n sigma g =
 (* display evar type: a context and a type *)
 let pr_evgl_sign gl =
   let ps = pr_named_context_of (evar_unfiltered_env gl) in
-  let _,l = list_filter2 (fun b c -> not b) (evar_filter gl,evar_context gl) in
+  let _,l = List.filter2 (fun b c -> not b) (evar_filter gl,evar_context gl) in
   let ids = List.rev (List.map pi1 l) in
   let warn =
     if ids = [] then mt () else
@@ -664,7 +664,7 @@ let print_one_inductive env mib ((_,i) as ind) =
   brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes
 
 let print_mutual_inductive env mind mib =
-  let inds = list_tabulate (fun x -> (mind,x)) (Array.length mib.mind_packets)
+  let inds = List.tabulate (fun x -> (mind,x)) (Array.length mib.mind_packets)
   in
   hov 0 (
     str (if mib.mind_finite then "Inductive " else "CoInductive ") ++
-- 
cgit v1.2.3