aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativevalues.mli
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-10-21 08:56:36 +0000
committerGitHub2020-10-21 08:56:36 +0000
commit637657847c6215e031947de042b927a9efd34edd (patch)
tree421b6b984b6d3aec4bc77e9e97dd6d7a6d2b2038 /kernel/nativevalues.mli
parent91e7863e64a5741b6530828c1642d765ddff41ae (diff)
parentc3cfb3c26241c374545380f08aa4345eb553000e (diff)
Merge PR #12955: Reroot primitive arrays on access
Reviewed-by: maximedenes
Diffstat (limited to 'kernel/nativevalues.mli')
-rw-r--r--kernel/nativevalues.mli4
1 files changed, 0 insertions, 4 deletions
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 08c5bd7126..b9b75a9d7c 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -344,7 +344,6 @@ val arrayget : t -> t -> t -> t -> t (* accu A t n *)
val arraydefault : t -> t -> t (* accu A t *)
val arrayset : t -> t -> t -> t -> t -> t (* accu A t n v *)
val arraycopy : t -> t -> t -> t (* accu A t *)
-val arrayreroot : t -> t -> t -> t (* accu A t *)
val arraylength : t -> t -> t -> t (* accu A t *)
val arrayinit : t -> t -> t -> t (* accu A n f def *)
val arraymap : t -> t -> t (* accu A B f t *)
@@ -364,8 +363,5 @@ val no_check_arrayset : t -> t -> t -> t
val no_check_arraycopy : t -> t
[@@ocaml.inline always]
-val no_check_arrayreroot : t -> t
-[@@ocaml.inline always]
-
val no_check_arraylength : t -> t
[@@ocaml.inline always]