From 9953fc3c125d0bdd39e3bd5801040f406f2e708f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 22 May 2018 08:58:53 +0200
Subject: Faster and cleaner fconstr-to-constr conversion function.

We untangle the implementation in several ways.
- No higher-order self argument function as there is only one caller.
- Compute composition of lifts + substitution on terms using a dedicated
  function instead of mk_clos followed by to_constr.
- Take more advantage of identity substitutions.
---
 kernel/cClosure.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/cClosure.mli')

diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 63daa4a7c3..f8f98f0abe 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -244,6 +244,6 @@ val kni: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
 val knr: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
 val kl : clos_infos -> fconstr infos_tab -> fconstr -> constr
 
-val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr
+val to_constr : lift -> fconstr -> constr
 
 (** End of cbn debug section i*)
-- 
cgit v1.2.3