diff options
| author | Pierre-Marie Pédrot | 2018-10-09 18:46:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-11 13:09:03 +0200 |
| commit | e2141cc741c2a77f05dabd9a8b48d9051d6d6cd4 (patch) | |
| tree | 961b9141945cb67435ef6434e90356e671d50e41 /kernel/cClosure.mli | |
| parent | 2f2d31d8408b4e15b193110309c4800a456cfb83 (diff) | |
Clean up CClosure code.
We take advantage of the separation of implementation from CBV to remove
constant code.
Diffstat (limited to 'kernel/cClosure.mli')
| -rw-r--r-- | kernel/cClosure.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 22c82f6d36..1ee4bccc25 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -218,8 +218,6 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> (** [unfold_reference] unfolds references in a [fconstr] *) val unfold_reference : clos_infos -> clos_tab -> table_key -> fconstr option -val eq_table_key : table_key -> table_key -> bool - (*********************************************************************** i This is for lazy debug *) |