4 files changed, 16 insertions, 9 deletions

diff --git a/kernel/context.ml b/kernel/context.ml
index d24922e18..930ab7508 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 79ddbe49b..ad6d645cd 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 77675bd58..e0bfb69ae 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 1469192b1..12c1529c8 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]