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
---
 kernel/inductive.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 58689a9263..d86abb435f 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -54,7 +54,7 @@ let inductive_params (mib,_) = mib.mind_nparams
 let ind_subst mind mib =
   let ntypes = mib.mind_ntypes in
   let make_Ik k = mkInd (mind,ntypes-k-1) in
-  list_tabulate make_Ik ntypes
+  List.tabulate make_Ik ntypes
 
 (* Instantiate inductives in constructor type *)
 let constructor_instantiate mind mib c =
@@ -272,7 +272,7 @@ let extended_rel_list n hyps =
   reln [] 1 hyps
 
 let build_dependent_inductive ind (_,mip) params =
-  let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+  let realargs,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
   applist
     (mkInd ind,
        List.map (lift mip.mind_nrealargs_ctxt) params
@@ -327,7 +327,7 @@ let build_branches_type ind (_,mip as specif) params p =
     let (args,ccl) = decompose_prod_assum typi in
     let nargs = rel_context_length args in
     let (_,allargs) = decompose_app ccl in
-    let (lparams,vargs) = list_chop (inductive_params specif) allargs in
+    let (lparams,vargs) = List.chop (inductive_params specif) allargs in
     let cargs =
       let cstr = ith_constructor_of_inductive ind (i+1) in
       let dep_cstr = applist (mkConstruct cstr,lparams@(local_rels args)) in
@@ -344,7 +344,7 @@ let build_case_type n p c realargs =
 let type_case_branches env (ind,largs) pj c =
   let specif = lookup_mind_specif env ind in
   let nparams = inductive_params specif in
-  let (params,realargs) = list_chop nparams largs in
+  let (params,realargs) = List.chop nparams largs in
   let p = pj.uj_val in
   let univ = is_correct_arity env c pj ind specif params in
   let lc = build_branches_type ind specif params p in
@@ -451,7 +451,7 @@ let push_var renv (x,ty,spec) =
     genv = spec:: renv.genv }
 
 let assign_var_spec renv (i,spec) =
-  { renv with genv = list_assign renv.genv (i-1) spec }
+  { renv with genv = List.assign renv.genv (i-1) spec }
 
 let push_var_renv renv (x,ty) =
   push_var renv (x,ty,lazy Not_subterm)
@@ -521,7 +521,7 @@ let branches_specif renv c_spec ci =
 		    vra
 	      | Dead_code -> Array.create nca Dead_code
 	      | _ -> Array.create nca Not_subterm) in
-	 list_tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca)
+	 List.tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca)
       car 
 
 (* [subterm_specif renv t] computes the recursive structure of [t] and
@@ -870,7 +870,7 @@ let check_one_cofix env nbfix def deftype =
             let lra = vlra.(i-1) in
             let mI = inductive_of_constructor cstr_kn in
 	    let (mib,mip) = lookup_mind_specif env mI in
-            let realargs = list_skipn mib.mind_nparams args in
+            let realargs = List.skipn mib.mind_nparams args in
             let rec process_args_of_constr = function
               | (t::lr), (rar::lrar) ->
                   if rar = mk_norec then
-- 
cgit v1.2.3