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
---
 plugins/funind/functional_principles_proofs.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins/funind/functional_principles_proofs.ml')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 8ea4be631c..0796930fca 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -93,7 +93,7 @@ let observe_tac s = observe_tac_stream (str s)
 
 let list_chop ?(msg="") n l =
   try
-    list_chop n l
+    List.chop n l
   with Failure (msg') ->
     failwith (msg ^ msg')
 
@@ -319,7 +319,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
 	      )
     in
     let new_type_of_hyp,ctxt_size,witness_fun =
-      list_fold_left_i
+      List.fold_left_i
 	(fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) ->
 	   try
 	     let witness = Intmap.find i sub in
@@ -1168,7 +1168,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		typess
 	    in
 	    let pte_to_fix,rev_info =
-	      list_fold_left_i
+	      List.fold_left_i
 		(fun i (acc_map,acc_info) (pte,_,_) ->
 		   let infos = info_array.(i) in
 		   let type_args,_ = decompose_prod infos.types in
@@ -1557,7 +1557,7 @@ let prove_principle_for_gen
 (* 	     str "real_rec_arg_num := " ++ int real_rec_arg_num ++ fnl () ++ *)
 (* 	     str "npost_rec_arg := " ++ int npost_rec_arg ); *)
   let (post_rec_arg,pre_rec_arg) =
-    Util.list_chop npost_rec_arg princ_info.args
+    Util.List.chop npost_rec_arg princ_info.args
   in
   let rec_arg_id =
     match List.rev post_rec_arg with
@@ -1624,7 +1624,7 @@ let prove_principle_for_gen
 	  Elim.h_decompose_and (mkVar hid);
 	  (fun g ->
 	     let new_hyps = pf_ids_of_hyps g in
-	     tcc_list := List.rev (list_subtract new_hyps (hid::hyps));
+	     tcc_list := List.rev (List.subtract new_hyps (hid::hyps));
 	     if !tcc_list = []
 	     then
 	       begin
-- 
cgit v1.2.3