From a53eeffbbb573dd8c354d5e68ac19dea5f511f79 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 22 Oct 2020 18:45:41 +0200
Subject: Add a fast path in CClosure stack zipping.

No need to zip the stack if the machine has made no progress.
---
 kernel/cClosure.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'kernel/cClosure.ml')

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 952237ab99..174125fc57 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -1535,7 +1535,12 @@ let whd_stack infos tab m stk = match Mark.red_state m.mark with
   knh infos m stk
 | Red | Cstr ->
   let k = kni infos tab m stk in
-  let () = if infos.i_cache.i_share then ignore (fapp_stack k) in (* to unlock Zupdates! *)
+  let () =
+    if infos.i_cache.i_share then
+      (* to unlock Zupdates! *)
+      let (m', stk') = k in
+      if not (m == m' && stk == stk') then ignore (zip m' stk')
+  in
   k
 
 let create_clos_infos ?univs ?(evars=fun _ -> None) flgs env =
-- 
cgit v1.2.3