diff options
| author | Matthieu Sozeau | 2020-04-06 14:42:12 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2020-04-06 14:42:12 +0200 |
| commit | 2089207415565e8a28816f53b61d9292d04f4c59 (patch) | |
| tree | 9d8edb9e90c93b767ef471ee76e1503624baa878 /kernel | |
| parent | 28c031158cee24faf782a7192032e29229aee4d4 (diff) | |
| parent | 5a961410854f01a4445b6605483d0b227279a1fd (diff) | |
Merge PR #11955: Use the kernel machine in whd_betaiota_deltazeta_for_iota_state
Reviewed-by: SkySkimmer
Reviewed-by: mattam82
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cClosure.ml | 2 | ||||
| -rw-r--r-- | kernel/cClosure.mli | 4 |
2 files changed, 6 insertions, 0 deletions
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 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*) |