From 2a4d71fc15dfa4916358e3eba5d37c1995a68f90 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 5 Nov 2013 20:01:03 +0000
Subject: Preventing useless allocations in Reductionops.instance.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17063 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/reductionops.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 41bd33dbcf..acd3a7eba7 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -797,6 +797,8 @@ let whd_meta sigma c = match kind_of_term c with
   | Meta p -> (try meta_value sigma p with Not_found -> c)
   | _ -> c
 
+let hid = Id.of_string "H"
+
 (* Try to replace all metas. Does not replace metas in the metas' values
  * Differs from (strong whd_meta). *)
 let plain_instance s c =
@@ -804,7 +806,7 @@ let plain_instance s c =
     | Meta p -> (try lift n (Metamap.find p s) with Not_found -> u)
     | App (f,l) when isCast f ->
         let (f,_,t) = destCast f in
-        let l' = Array.map (irec n) l in
+        let l' = CArray.Fun1.smartmap irec n l in
         (match kind_of_term f with
         | Meta p ->
 	    (* Don't flatten application nodes: this is used to extract a
@@ -813,8 +815,8 @@ let plain_instance s c =
 	    (try let g = Metamap.find p s in
 	    match kind_of_term g with
             | App _ ->
-                let h = Id.of_string "H" in
-                mkLetIn (Name h,g,t,mkApp(mkRel 1,Array.map (lift 1) l'))
+                let l' = CArray.Fun1.smartmap lift 1 l' in
+                mkLetIn (Name hid,g,t,mkApp(mkRel 1, l'))
             | _ -> mkApp (g,l')
 	    with Not_found -> mkApp (f,l'))
         | _ -> mkApp (irec n f,l'))
-- 
cgit v1.2.3