aboutsummaryrefslogtreecommitdiff
path: root/kernel/closure.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/closure.mli')
-rw-r--r--kernel/closure.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 8c80324238..e045bd60fc 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -202,5 +202,6 @@ val knr: clos_infos -> fconstr -> fconstr stack -> fconstr * fconstr stack
val kl : clos_infos -> fconstr -> constr
val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr
+val optimise_closure : fconstr subs -> constr -> fconstr subs * constr
(* End of cbn debug section i*)