aboutsummaryrefslogtreecommitdiff
path: root/kernel/vmvalues.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/vmvalues.mli')
-rw-r--r--kernel/vmvalues.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index f6efd49cfc..ee3e2bd5fc 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -181,7 +181,6 @@ val rec_args : vfix -> int array
val first_fix : vfix -> vfix
val fix_types : vfix -> tcode array
val cofix_types : vcofix -> tcode array
-external offset_closure_fix : vfix -> int -> vm_env = "coq_offset_closure"
val mk_fix_body : int -> int -> vfix -> vfun array
(** CoFix *)