From 914d19f19cd73d1794c0160bd6e7358c13eba630 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sat, 23 Mar 2013 15:05:26 +0000
Subject: Minor code cleaning in CArray / CList.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16351 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/decl_mode/decl_interp.ml      | 5 ++---
 plugins/decl_mode/decl_proof_instr.ml | 2 +-
 2 files changed, 3 insertions(+), 4 deletions(-)

(limited to 'plugins/decl_mode')

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 3cc0686ada..9d34dc99a1 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -341,9 +341,8 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
 	(fun (loc,(id,_)) ->
 	   GVar (loc,id)) params in
     let dum_args=
-      List.tabulate
-	(fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false)))
-	oib.Declarations.mind_nrealargs in
+      List.init oib.Declarations.mind_nrealargs
+	(fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false))) in
       glob_app(Loc.ghost,rind,rparams@rparams_rec@dum_args) in
   let pat_vars,aliases,patt = interp_pattern env pat in
   let inject = function
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 1ae8419c83..2ef2c97562 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1190,7 +1190,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	  match List.assoc id args with
 	      [None,br_args] -> 
 		let all_metas = 
-		  List.tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps)  in
+		  List.init (nparams + nhyps) (fun n -> mkMeta (succ n))  in
 		let param_metas,hyp_metas = List.chop nparams all_metas in
 		  tclTHEN
 		    (tclDO nhrec introf)
-- 
cgit v1.2.3