diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-08 17:47:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-21 19:36:26 +0200 |
| commit | 3fb9633ae5aea9d3704694490770e6e614da8c5d (patch) | |
| tree | 936cc378abe67b62eb303e0306bac06b5c3bfc5c /kernel/cClosure.mli | |
| parent | d6eb4a26648817f6b034e95c02622cadf0fa65ca (diff) | |
Simplify the newring hack.
The new implementation is 100% compatible with the previous one, but it
is more compact and does not use a tricky translation function from the
kernel.
Diffstat (limited to 'kernel/cClosure.mli')
| -rw-r--r-- | kernel/cClosure.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index e2f5a3b82..63daa4a7c 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -239,9 +239,6 @@ val lift_fconstr_vect : int -> fconstr array -> fconstr array val mk_clos : fconstr subs -> constr -> fconstr val mk_clos_vect : fconstr subs -> constr array -> fconstr array -val mk_clos_deep : - (fconstr subs -> constr -> fconstr) -> - fconstr subs -> constr -> fconstr val kni: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack val knr: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack |