Removing useless casts between arrays and lists.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16659 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 27 insertions, 17 deletions

diff --git a/kernel/context.ml b/kernel/context.ml
index d24922e189..930ab75081 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -93,11 +93,11 @@ let named_context_equal = List.equal eq_named_declaration
 let vars_of_named_context = List.map (fun (id,_,_) -> id)
 
 let instance_from_named_context sign =
-  let rec inst_rec = function
-    | (id,None,_) :: sign -> Constr.mkVar id :: inst_rec sign
-    | _ :: sign -> inst_rec sign
-    | [] -> [] in
-  Array.of_list (inst_rec sign)
+  let filter = function
+  | (id, None, _) -> Some (Constr.mkVar id)
+  | (_, Some _, _) -> None
+  in
+  List.map_filter filter sign
 
 let fold_named_context f l ~init = List.fold_right f l init
 let fold_named_context_reverse f ~init l = List.fold_left f init l
diff --git a/kernel/context.mli b/kernel/context.mli
index 79ddbe49b1..ad6d645cd3 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -75,7 +75,7 @@ val fold_named_context_reverse :
   ('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a
 
 (** {6 Section-related auxiliary functions } *)
-val instance_from_named_context : named_context -> Constr.t array
+val instance_from_named_context : named_context -> Constr.t list
 
 (** {6 ... } *)
 (** Signatures of ordered optionally named variables, intended to be
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 77675bd589..e0bfb69aee 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -549,7 +549,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
 let check_positivity kn env_ar params inds =
   let ntypes = Array.length inds in
   let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in
-  let lra_ind = List.rev (Array.to_list rc) in
+  let lra_ind = Array.rev_to_list rc in
   let lparams = rel_context_length params in
   let nmr = rel_context_nhyps params in
   let check_one i (_,lcnames,lc,(sign,_)) =
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 1469192b11..12c1529c8b 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -131,8 +131,15 @@ let substkey = Profile.declare_profile "substn_many";;
 let substn_many lamv n c = Profile.profile3 substkey substn_many lamv n c;;
 *)
 
-let substnl laml n =
-  substn_many (Array.map make_substituend (Array.of_list laml)) n
+let make_subst = function
+| [] -> [||]
+| hd :: tl ->
+  let subst = Array.make (1 + List.length tl) (make_substituend hd) in
+  let iteri i x = Array.unsafe_set subst (succ i) (make_substituend x) in
+  let () = CList.iteri iteri tl in
+  subst
+
+let substnl laml n = substn_many (make_subst laml) n
 let substl laml = substnl laml 0
 let subst1 lam = substl [lam]
 
diff --git a/library/declare.ml b/library/declare.ml
index d664ebd0cb..e2831b8626 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -314,7 +314,7 @@ let fixpoint_message indexes l =
 		  spc () ++ str "are recursively defined" ++
 		  match indexes with
 		    | Some a -> spc () ++ str "(decreasing respectively on " ++
-			prlist_with_sep pr_comma pr_rank (Array.to_list a) ++
+			prvect_with_sep pr_comma pr_rank a ++
 			str " arguments)"
 		    | None -> mt ()))
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 61f618c409..265ba4b144 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -307,7 +307,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
 	 sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
       let hyps = evar_filtered_context (Evd.find !evdref evk) in
       let args = match instopt with
-        | None -> instance_from_named_context hyps
+        | None -> Array.of_list (instance_from_named_context hyps)
         | Some inst -> failwith "Evar subtitutions not implemented" in
       let c = mkEvar (evk, args) in
       let j = (Retyping.get_judgment_of env !evdref c) in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 4b08f7517a..76587a3408 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Names
 open Declarations
 open Term
@@ -59,7 +60,7 @@ let type_constructor mind mib typ params =
   if nparams = 0 then ctyp
   else
     let _,ctyp = decompose_prod_n nparams ctyp in
-    substl (List.rev (Array.to_list params)) ctyp
+    substl (Array.rev_to_list params) ctyp
 
 
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f357da8178..228498a476 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -657,7 +657,8 @@ let bring_hyps hyps =
     (fun gl ->
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps (pf_concl gl) in
       let f = mkCast (Evarutil.mk_new_meta(),DEFAULTcast, newcl) in
-      refine_no_check (mkApp (f, instance_from_named_context hyps)) gl)
+      let args = Array.of_list (instance_from_named_context hyps) in
+      refine_no_check (mkApp (f, args)) gl)
 
 let resolve_classes gl =
   let env = pf_env gl and evd = project gl in
@@ -1624,7 +1625,7 @@ let generalize_dep ?(with_let=false) c gl =
     else None
   in
   let cl'' = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous) cl' in
-  let args = Array.to_list (instance_from_named_context to_quantify_rev) in
+  let args = instance_from_named_context to_quantify_rev in
   tclTHEN
     (apply_type cl'' (if Option.is_empty body then c::args else args))
     (thin (List.rev tothin'))
@@ -1753,7 +1754,7 @@ let letin_tac with_eq name c occs gl =
   let (depdecls,marks,ccl)= letin_abstract id c occs gl in
   let t = pf_type_of gl c in
   let tmpcl = List.fold_right mkNamedProd_or_LetIn depdecls ccl in
-  let args = Array.to_list (instance_from_named_context depdecls) in
+  let args = instance_from_named_context depdecls in
   let newcl = mkNamedLetIn id c t tmpcl in
   let lastlhyp = if marks=[] then None else snd (List.hd marks) in
   tclTHENLIST
@@ -3594,7 +3595,7 @@ let abstract_subproof id tac gl =
   let cst = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true id decl in
   let lem = mkConst cst in
   exact_no_check
-    (applist (lem,List.rev (Array.to_list (instance_from_named_context sign))))
+    (applist (lem,List.rev (instance_from_named_context sign)))
     gl
 
 let tclABSTRACT name_op tac gl =
@@ -3629,7 +3630,7 @@ let admit_as_an_axiom gl =
   let gl =
     exact_no_check
       (applist (axiom,
-              List.rev (Array.to_list (instance_from_named_context sign))))
+              List.rev (instance_from_named_context sign)))
     gl in
   Pp.feedback Interface.AddedAxiom;
   gl
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 8d9e73e6d7..b9ffbaea55 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -39,6 +39,7 @@ let abstract_inductive hyps nparams inds =
   let ntyp = List.length inds in
   let nhyp = named_context_length hyps in
   let args = instance_from_named_context (List.rev hyps) in
+  let args = Array.of_list args in
   let subs = List.init ntyp (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) in
   let inds' =
     List.map