From 328279514e65f47a689e2d23f132c43c86870c05 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sat, 2 Nov 2013 15:25:09 +0000
Subject: Closure: fix an issue with r16959 spotted by Matthieu

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

(limited to 'kernel')

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 187ea4478c..e1f3cd582c 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -534,8 +534,9 @@ and compact_vect s v k =
     let () = rs := s in
     a
   in
-  (** Do we really rely on execution order? *)
-  (Array.smartmap map v, !rs)
+  (** Do we really rely on execution order in the smartmap ? *)
+  let v' = Array.smartmap map v in
+  (v', !rs)
 
 (* Computes the minimal environment of a closure.
    Idea: if the subs is not identity, the term will have to be
-- 
cgit v1.2.3