diff options
| author | Pierre-Marie Pédrot | 2020-03-28 09:28:00 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-03 19:32:13 +0200 |
| commit | b5f2b861a3d391716e976469a1a100536550bef8 (patch) | |
| tree | 0ffa7c9b0c116f0cc7a592f4a05f4a0ce080d8f1 /kernel/cClosure.mli | |
| parent | c20139f870430d856d6b891a7129ee72d7b54ff4 (diff) | |
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.
Diffstat (limited to 'kernel/cClosure.mli')
| -rw-r--r-- | kernel/cClosure.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 9e94248113..79092813bc 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -227,6 +227,10 @@ val kni: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack val knr: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack val kl : clos_infos -> clos_tab -> fconstr -> constr +val zip : fconstr -> stack -> fconstr + +val term_of_process : fconstr -> stack -> constr + val to_constr : lift -> fconstr -> constr (** End of cbn debug section i*) |