Remove occurrences of Parray.reroot.

11 files changed, 2 insertions, 34 deletions

diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index 314cb54d1d..5cd91b4e74 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -58,7 +58,6 @@ type t =
   | Arraydefault
   | Arrayset
   | Arraycopy
-  | Arrayreroot
   | Arraylength
 
 let parse = function
@@ -110,7 +109,6 @@ let parse = function
   | "array_set" -> Arrayset
   | "array_length" -> Arraylength
   | "array_copy" -> Arraycopy
-  | "array_reroot" -> Arrayreroot
   | _ -> raise Not_found
 
 let equal (p1 : t) (p2 : t) =
@@ -164,8 +162,7 @@ let hash = function
   | Arraydefault -> 45
   | Arrayset -> 46
   | Arraycopy -> 47
-  | Arrayreroot -> 48
-  | Arraylength -> 49
+  | Arraylength -> 48
 
 (* Should match names in nativevalues.ml *)
 let to_string = function
@@ -216,7 +213,6 @@ let to_string = function
   | Arraydefault -> "arraydefault"
   | Arrayset -> "arrayset"
   | Arraycopy -> "arraycopy"
-  | Arrayreroot -> "arrayreroot"
   | Arraylength -> "arraylength"
 
 type const =
@@ -302,7 +298,6 @@ let types =
   | Arraydefault -> [array_ty; PITT_param 1]
   | Arrayset -> [array_ty; int_ty; PITT_param 1; array_ty]
   | Arraycopy -> [array_ty; array_ty]
-  | Arrayreroot -> [array_ty; array_ty]
   | Arraylength -> [array_ty; int_ty]
 
 let one_param =
@@ -360,7 +355,6 @@ let params = function
   | Arraydefault
   | Arrayset
   | Arraycopy
-  | Arrayreroot
   | Arraylength -> one_param
 
 let nparams x = List.length (params x)
@@ -414,7 +408,6 @@ let univs = function
   | Arraydefault
   | Arrayset
   | Arraycopy
-  | Arrayreroot
   | Arraylength -> one_univ
 
 type arg_kind =
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli
index 41b3bff465..0db643faf4 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -56,7 +56,6 @@ type t =
   | Arraydefault
   | Arrayset
   | Arraycopy
-  | Arrayreroot
   | Arraylength
 
 (** Can raise [Not_found].
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 9e17f97a56..05c98e4b87 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -739,15 +739,6 @@ let arraycopy accu vA t =
     no_check_arraycopy t
   else accu vA t
 
-let no_check_arrayreroot t =
-  of_parray (Parray.reroot (to_parray t))
-[@@ocaml.inline always]
-
-let arrayreroot accu vA t =
-  if is_parray t then
-    no_check_arrayreroot t
-  else accu vA t
-
 let no_check_arraylength t =
   mk_uint (Parray.length (to_parray t))
 [@@ocaml.inline always]
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]
diff --git a/kernel/parray.mli b/kernel/parray.mli
index 0276278bd0..8b6565c159 100644
--- a/kernel/parray.mli
+++ b/kernel/parray.mli
@@ -19,7 +19,6 @@ val default : 'a t -> 'a
 val make    : Uint63.t -> 'a -> 'a t
 val init    : Uint63.t -> (int -> 'a) -> 'a -> 'a t
 val copy    : 'a t -> 'a t
-val reroot  : 'a t -> 'a t
 
 val map : ('a -> 'b) -> 'a t -> 'b t
 
diff --git a/kernel/primred.ml b/kernel/primred.ml
index 90eeeb9be7..f158cfacea 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -365,11 +365,6 @@ struct
       let t = get_parray evd args 1 in
       let t' = Parray.copy t in
       E.mkArray env u t' ty
-    | Arrayreroot ->
-      let ar = E.get args 1 in
-      let t = E.get_parray evd ar in
-      let _ = Parray.reroot t in
-      ar
     | Arraylength ->
       let t = get_parray evd args 1 in
       E.mkInt env (Parray.length t)
diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml
index 375b1aface..16a0f42664 100644
--- a/kernel/vmbytegen.ml
+++ b/kernel/vmbytegen.ml
@@ -508,7 +508,6 @@ let is_caml_prim = let open CPrimitives in function
   | Arraydefault
   | Arrayset
   | Arraycopy
-  | Arrayreroot
   | Arraylength -> true
   | _ -> false
 
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
index f913cb906c..ec8601edc9 100644
--- a/kernel/vmemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -262,7 +262,7 @@ let check_prim_op = function
   | Arraymake -> opISINT_CAML_CALL2
   | Arrayget -> opISARRAY_INT_CAML_CALL2
   | Arrayset -> opISARRAY_INT_CAML_CALL3
-  | Arraydefault | Arraycopy | Arrayreroot | Arraylength ->
+  | Arraydefault | Arraycopy | Arraylength ->
       opISARRAY_CAML_CALL1
 
 let emit_instr env = function
diff --git a/kernel/vmsymtable.ml b/kernel/vmsymtable.ml
index 4ad830a298..9d80dc578b 100644
--- a/kernel/vmsymtable.ml
+++ b/kernel/vmsymtable.ml
@@ -69,7 +69,6 @@ let parray_get = set_global Vmvalues.parray_get
 let parray_get_default = set_global Vmvalues.parray_get_default
 let parray_set = set_global Vmvalues.parray_set
 let parray_copy = set_global Vmvalues.parray_copy
-let parray_reroot = set_global Vmvalues.parray_reroot
 let parray_length = set_global Vmvalues.parray_length
 
 (* table pour les structured_constant et les annotations des switchs *)
@@ -135,7 +134,6 @@ let slot_for_caml_prim =
   | Arraydefault -> parray_get_default
   | Arrayset -> parray_set
   | Arraycopy -> parray_copy
-  | Arrayreroot -> parray_reroot
   | Arraylength -> parray_length
   | _ -> assert false
 
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 0678f37a0b..2068133b10 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -700,5 +700,4 @@ let parray_get = Obj.magic Parray.get
 let parray_get_default = Obj.magic Parray.default
 let parray_set = Obj.magic Parray.set
 let parray_copy = Obj.magic Parray.copy
-let parray_reroot = Obj.magic Parray.reroot
 let parray_length = Obj.magic Parray.length
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index 6632dc46b2..d15595766a 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -204,5 +204,4 @@ val parray_get : values
 val parray_get_default : values
 val parray_set : values
 val parray_copy : values
-val parray_reroot : values
 val parray_length : values