Prevent [Evarutil.whd_head_evar] from uselessly reallocating arrays.

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

1 files changed, 16 insertions, 4 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 6381c29a16..8bf1ecf976 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -144,15 +144,27 @@ let head_evar =
 let whd_head_evar_stack sigma c =
   let rec whrec (c, l as s) =
     match kind_of_term c with
-      | Evar (evk,args as ev) when Evd.is_defined sigma evk
-	  -> whrec (existential_value sigma ev, l)
+      | Evar (evk,args as ev) ->
+        let v =
+          try Some (existential_value sigma ev)
+          with NotInstantiatedEvar | Not_found  -> None in
+        begin match v with
+        | None -> s
+        | Some c -> whrec (c, l)
+        end
       | Cast (c,_,_) -> whrec (c, l)
-      | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
+      | App (f,args) -> whrec (f, args :: l)
       | _ -> s
   in
   whrec (c, [])
 
-let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c)
+let whd_head_evar sigma c =
+  let (f, args) = whd_head_evar_stack sigma c in
+  (** optim: don't reallocate if empty/singleton *)
+  match args with
+  | [] -> f
+  | [arg] -> mkApp (f, arg)
+  | _ -> mkApp (f, Array.concat args)
 
 (**********************)
 (* Creating new metas *)