From b5f2b861a3d391716e976469a1a100536550bef8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 28 Mar 2020 09:28:00 +0100
Subject: Be cleverer and do not hopelessly rezip a term when not needed.

A quick analysis showed that most of the calls to whd do not lead to a
term which further triggers reduction, so there is no point in refolding
a potentiall huge term for no reason.
---
 kernel/cClosure.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/cClosure.ml')

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 1316dfe069..c31cdae6f5 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -678,6 +678,8 @@ let rec zip m stk =
 
 let fapp_stack (m,stk) = zip m stk
 
+let term_of_process c stk = term_of_fconstr (zip c stk)
+
 (*********************************************************************)
 
 (* The assertions in the functions below are granted because they are
-- 
cgit v1.2.3