Primitive persistent arrays

Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
author: Maxime Dénès 2020-02-03 18:19:42 +0100
committer: Maxime Dénès 2020-07-06 11:22:43 +0200
commit: 0ea2d0ff4ed84e1cc544c958b8f6e98f6ba2e9b6 (patch)
tree: fbad060c3c2e29e81751dea414c898b5cb0fa22d /kernel
parent: cf388fdb679adb88a7e8b3122f65377552d2fb94 (diff)
52 files changed, 1499 insertions, 346 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 306643f758..814cdfe1d8 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -75,6 +75,8 @@ void init_arity () {
     arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]=1;
   /* instruction with two operands */
   arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
+  arity[ISARRAY_CAML_CALL1]=arity[ISINT_CAML_CALL2]=
+  arity[ISARRAY_INT_CAML_CALL2]=arity[ISARRAY_INT_CAML_CALL3]=
   arity[PROJ]=2;
   /* instruction with four operands */
   arity[MAKESWITCHBLOCK]=4;
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 7588c1ce07..9921208e04 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -22,6 +22,7 @@
 #include <caml/memory.h>
 #include <caml/signals.h>
 #include <caml/version.h>
+#include <caml/callback.h>
 
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
@@ -111,7 +112,8 @@ if (sp - num_args < coq_stack_threshold) {                                     \
 /* GC interface */
 #define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; }
 #define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; }
-
+#define Setup_for_caml_call { *--sp = coq_env; coq_sp = sp; }
+#define Restore_after_caml_call { sp = coq_sp; coq_env = *sp++; }
 
 /* Register optimization.
    Some compilers underestimate the use of the local variables representing
@@ -1771,6 +1773,71 @@ value coq_interprete
         Next;
       }
 
+
+      Instruct(ISINT_CAML_CALL2) {
+        value arg;
+        print_instr("ISINT_CAML_CALL2");
+        if (Is_uint63(accu)) {
+          pc++;
+          print_int(*pc);
+          arg = sp[0];
+          Setup_for_caml_call;
+          accu = caml_callback2(Field(coq_global_data, *pc), accu, arg);
+          Restore_after_caml_call;
+          sp += 1;
+          pc++;
+        } else pc += *pc;
+        Next;
+      }
+
+      Instruct(ISARRAY_CAML_CALL1) {
+        print_instr("ISARRAY_CAML_CALL1");
+              if (Is_coq_array(accu)) {
+                pc++;
+                Setup_for_caml_call;
+                print_int(*pc);
+                accu = caml_callback(Field(coq_global_data, *pc),accu);
+                Restore_after_caml_call;
+                pc++;
+              }
+              else pc += *pc;
+              Next;
+      }
+
+      Instruct(ISARRAY_INT_CAML_CALL2) {
+        value arg;
+        print_instr("ISARRAY_INT_CAML_CALL2");
+          if (Is_coq_array(accu) && Is_uint63(sp[0])) {
+            pc++;
+            arg = sp[0];
+            Setup_for_caml_call;
+            print_int(*pc);
+            accu = caml_callback2(Field(coq_global_data, *pc), accu, arg);
+            Restore_after_caml_call;
+            sp += 1;
+            pc++;
+          } else pc += *pc;
+          Next;
+      }
+
+      Instruct(ISARRAY_INT_CAML_CALL3) {
+        value arg1;
+        value arg2;
+        print_instr("ISARRAY_INT_CAML_CALL3");
+        if (Is_coq_array(accu) && Is_uint63(sp[0])) {
+          pc++;
+          arg1 = sp[0];
+          arg2 = sp[1];
+          Setup_for_caml_call;
+          print_int(*pc);
+          accu = caml_callback3(Field(coq_global_data, *pc),accu, arg1, arg2);
+          Restore_after_caml_call;
+          sp += 2;
+          pc++;
+        } else pc += *pc;
+        Next;
+      }
+
 /* Debugging and machine control */
 
       Instruct(STOP){
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index b027673ac7..86ae6295fd 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -33,6 +33,9 @@
 #define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG))
 #define Is_double(v) (Tag_val(v) == Double_tag)
 
+/* coq array */
+#define Is_coq_array(v) (Is_block(v) && (Wosize_val(v) == 1))
+
 /* coq values for primitive operations */
 #define coq_tag_C1 2
 #define coq_tag_C0 1
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 9640efd8eb..a23ef8fdca 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -350,6 +350,7 @@ and fterm =
   | FEvar of existential * fconstr subs
   | FInt of Uint63.t
   | FFloat of Float64.t
+  | FArray of Univ.Instance.t * fconstr Parray.t * fconstr
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs
   | FLOCKED
@@ -456,7 +457,7 @@ let rec lft_fconstr n ft =
     | FLIFT(k,m) -> lft_fconstr (n+k) m
     | FLOCKED -> assert false
     | FFlex (RelKey _) | FAtom _ | FApp _ | FProj _ | FCaseT _ | FCaseInvert _ | FProd _
-      | FLetIn _ | FEvar _ | FCLOS _ -> {mark=ft.mark; term=FLIFT(n,ft)}
+      | FLetIn _ | FEvar _ | FCLOS _ | FArray _ -> {mark=ft.mark; term=FLIFT(n,ft)}
 let lift_fconstr k f =
   if Int.equal k 0 then f else lft_fconstr k f
 let lift_fconstr_vect k v =
@@ -518,11 +519,13 @@ let mk_clos e t =
     | Construct kn -> {mark = mark Cstr Unknown; term = FConstruct kn }
     | Int i -> {mark = mark Cstr Unknown; term = FInt i}
     | Float f -> {mark = mark Cstr Unknown; term = FFloat f}
-    | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) ->
+    | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _|Array _) ->
         {mark = mark Red Unknown; term = FCLOS(t,e)}
 
 let inject c = mk_clos (subs_id 0) c
 
+(************************************************************************)
+
 (** Hand-unrolling of the map function to bypass the call to the generic array
     allocation *)
 let mk_clos_vect env v = match v with
@@ -558,7 +561,7 @@ let ref_value_cache ({ i_cache = cache; _ }) tab ref =
         in
         Def (inject body)
       with
-      | NotEvaluableConst (IsPrimitive op) (* Const *) -> Primitive op
+      | NotEvaluableConst (IsPrimitive (_u,op)) (* Const *) -> Primitive op
       | Not_found (* List.assoc *)
       | NotEvaluableConst _ (* Const *)
         -> Undef None
@@ -626,7 +629,7 @@ let rec to_constr lfts v =
                     subst_constr subs f)
     | FEvar ((ev,args),env) ->
       let subs = comp_subs lfts env in
-        mkEvar(ev,List.map (fun a -> subst_constr subs a) args)
+        mkEvar(ev, List.map (fun a -> subst_constr subs a) args)
     | FLIFT (k,a) -> to_constr (el_shft k lfts) a
 
     | FInt i ->
@@ -634,6 +637,11 @@ let rec to_constr lfts v =
     | FFloat f ->
         Constr.mkFloat f
 
+    | FArray (u,t,ty) ->
+      let ty = to_constr lfts ty in
+      let init i = to_constr lfts (Parray.get t (Uint63.of_int i)) in
+      mkArray(u,Array.init (Parray.length_int t) init, to_constr lfts (Parray.default t),ty)
+
     | FCLOS (t,env) ->
       if is_subs_id env && is_lift_id lfts then t
       else
@@ -931,57 +939,6 @@ let unfold_projection info p =
     Some (Zproj (Projection.repr p))
   else None
 
-(*********************************************************************)
-(* A machine that inspects the head of a term until it finds an
-   atom or a subterm that may produce a redex (abstraction,
-   constructor, cofix, letin, constant), or a neutral term (product,
-   inductive) *)
-let rec knh info m stk =
-  match m.term with
-    | FLIFT(k,a) -> knh info a (zshift k stk)
-    | FCLOS(t,e) -> knht info e t (zupdate info m stk)
-    | FLOCKED -> assert false
-    | FApp(a,b) -> knh info a (append_stack b (zupdate info m stk))
-    | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate info m stk)
-    | FFix(((ri,n),_),_) ->
-        (match get_nth_arg m ri.(n) stk with
-             (Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk')
-           | (None, stk') -> (m,stk'))
-    | FProj (p,c) ->
-      (match unfold_projection info p with
-       | None -> (m, stk)
-       | Some s -> knh info c (s :: zupdate info m stk))
-
-(* cases where knh stops *)
-    | (FFlex _|FLetIn _|FConstruct _|FEvar _|FCaseInvert _|
-       FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _|FInt _|FFloat _) ->
-        (m, stk)
-
-(* The same for pure terms *)
-and knht info e t stk =
-  match kind t with
-    | App(a,b) ->
-        knht info e a (append_stack (mk_clos_vect e b) stk)
-    | Case(ci,p,NoInvert,t,br) ->
-        knht info e t (ZcaseT(ci, p, br, e)::stk)
-    | Case(ci,p,CaseInvert{univs;args},t,br) ->
-      let term = FCaseInvert (ci, p, (univs,Array.map (mk_clos e) args), mk_clos e t, br, e) in
-      { mark = mark Red Unknown; term }, stk
-    | Fix fx -> knh info { mark = mark Cstr Unknown; term = FFix (fx, e) } stk
-    | Cast(a,_,_) -> knht info e a stk
-    | Rel n -> knh info (clos_rel e n) stk
-    | Proj (p, c) -> knh info { mark = mark Red Unknown; term = FProj (p, mk_clos e c) } stk
-    | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _ | Int _|Float _) -> (mk_clos e t, stk)
-    | CoFix cfx -> { mark = mark Cstr Unknown; term = FCoFix (cfx,e) }, stk
-    | Lambda _ -> { mark = mark Cstr Unknown; term = mk_lambda e t }, stk
-    | Prod (n, t, c) ->
-      { mark = mark Whnf KnownR; term = FProd (n, mk_clos e t, c, e) }, stk
-    | LetIn (n,b,t,c) ->
-      { mark = mark Red Unknown; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk
-    | Evar ev -> { mark = mark Red Unknown; term = FEvar (ev, e) }, stk
-
-let inject c = mk_clos (subs_id 0) c
-
 (************************************************************************)
 (* Reduction of Native operators                                        *)
 
@@ -992,6 +949,7 @@ module FNativeEntries =
     type elem = fconstr
     type args = fconstr array
     type evd = unit
+    type uinstance = Univ.Instance.t
 
     let get = Array.get
 
@@ -1005,6 +963,11 @@ module FNativeEntries =
       | FFloat f -> f
       | _ -> raise Primred.NativeDestKO
 
+    let get_parray () e =
+      match [@ocaml.warning "-4"] e.term with
+      | FArray (_u,t,_ty) -> t
+      | _ -> raise Not_found
+
     let dummy = {mark = mark Norm KnownR; term = FRel 0}
 
     let current_retro = ref Retroknowledge.empty
@@ -1133,6 +1096,17 @@ module FNativeEntries =
         frefl := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs crefl) }
       | None -> defined_refl := false
 
+    let defined_array = ref false
+
+    let farray = ref dummy
+
+    let init_array retro =
+      match retro.Retroknowledge.retro_array with
+      | Some c ->
+        defined_array := true;
+        farray := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) }
+      | None -> defined_array := false
+
     let init env =
       current_retro := env.retroknowledge;
       init_int !current_retro;
@@ -1143,7 +1117,8 @@ module FNativeEntries =
       init_cmp !current_retro;
       init_f_cmp !current_retro;
       init_f_class !current_retro;
-      init_refl !current_retro
+      init_refl !current_retro;
+      init_array !current_retro
 
     let check_env env =
       if not (!current_retro == env.retroknowledge) then init env
@@ -1180,6 +1155,10 @@ module FNativeEntries =
       check_env env;
       assert (!defined_f_class)
 
+    let check_array env =
+      check_env env;
+      assert (!defined_array)
+
     let mkInt env i =
       check_int env;
       { mark = mark Cstr KnownR; term = FInt i }
@@ -1269,10 +1248,70 @@ module FNativeEntries =
     let mkNaN env =
       check_f_class env;
       !fNaN
+
+    let mkArray env u t ty =
+      check_array env;
+      { mark = mark Whnf KnownR; term = FArray (u,t,ty)}
+
   end
 
 module FredNative = RedNative(FNativeEntries)
 
+(*********************************************************************)
+(* A machine that inspects the head of a term until it finds an
+   atom or a subterm that may produce a redex (abstraction,
+   constructor, cofix, letin, constant), or a neutral term (product,
+   inductive) *)
+let rec knh info m stk =
+  match m.term with
+    | FLIFT(k,a) -> knh info a (zshift k stk)
+    | FCLOS(t,e) -> knht info e t (zupdate info m stk)
+    | FLOCKED -> assert false
+    | FApp(a,b) -> knh info a (append_stack b (zupdate info m stk))
+    | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate info m stk)
+    | FFix(((ri,n),_),_) ->
+        (match get_nth_arg m ri.(n) stk with
+             (Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk')
+           | (None, stk') -> (m,stk'))
+    | FProj (p,c) ->
+      (match unfold_projection info p with
+       | None -> (m, stk)
+       | Some s -> knh info c (s :: zupdate info m stk))
+
+(* cases where knh stops *)
+    | (FFlex _|FLetIn _|FConstruct _|FEvar _|FCaseInvert _|
+       FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _|FInt _|FFloat _|FArray _) ->
+        (m, stk)
+
+(* The same for pure terms *)
+and knht info e t stk =
+  match kind t with
+    | App(a,b) ->
+        knht info e a (append_stack (mk_clos_vect e b) stk)
+    | Case(ci,p,NoInvert,t,br) ->
+        knht info e t (ZcaseT(ci, p, br, e)::stk)
+    | Case(ci,p,CaseInvert{univs;args},t,br) ->
+      let term = FCaseInvert (ci, p, (univs,Array.map (mk_clos e) args), mk_clos e t, br, e) in
+      { mark = mark Red Unknown; term }, stk
+    | Fix fx -> knh info { mark = mark Cstr Unknown; term = FFix (fx, e) } stk
+    | Cast(a,_,_) -> knht info e a stk
+    | Rel n -> knh info (clos_rel e n) stk
+    | Proj (p, c) -> knh info { mark = mark Red Unknown; term = FProj (p, mk_clos e c) } stk
+    | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _ | Int _|Float _) -> (mk_clos e t, stk)
+    | CoFix cfx -> { mark = mark Cstr Unknown; term = FCoFix (cfx,e) }, stk
+    | Lambda _ -> { mark = mark Cstr Unknown; term = mk_lambda e t }, stk
+    | Prod (n, t, c) ->
+      { mark = mark Whnf KnownR; term = FProd (n, mk_clos e t, c, e) }, stk
+    | LetIn (n,b,t,c) ->
+      { mark = mark Red Unknown; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk
+    | Evar ev -> { mark = mark Red Unknown; term = FEvar (ev, e) }, stk
+    | Array(u,t,def,ty) ->
+      let len = Array.length t in
+      let ty = mk_clos e ty in
+      let t = Parray.init (Uint63.of_int len) (fun i -> mk_clos e t.(i)) (mk_clos e def) in
+      let term = FArray (u,t,ty) in
+      knh info { mark = mark Cstr Unknown; term } stk
+
 (************************************************************************)
 
 let conv : (clos_infos -> clos_tab -> fconstr -> fconstr -> bool) ref
@@ -1286,7 +1325,7 @@ let rec knr info tab m stk =
       (match get_args n tys f e stk with
           Inl e', s -> knit info tab e' f s
         | Inr lam, s -> (lam,s))
-  | FFlex(ConstKey (kn,_ as c)) when red_set info.i_flags (fCONST kn) ->
+  | FFlex(ConstKey (kn,_u as c)) when red_set info.i_flags (fCONST kn) ->
       (match ref_value_cache info tab (ConstKey c) with
         | Def v -> kni info tab v stk
         | Primitive op when check_native_args op stk ->
@@ -1335,15 +1374,16 @@ let rec knr info tab m stk =
       (match info.i_cache.i_sigma ev with
           Some c -> knit info tab env c stk
         | None -> (m,stk))
-  | FInt _ | FFloat _ ->
+  | FInt _ | FFloat _ | FArray _ ->
     (match [@ocaml.warning "-4"] strip_update_shift_app m stk with
-     | (_, _, Zprimitive(op,c,rargs,nargs)::s) ->
+     | (_, _, Zprimitive(op,(_,u as c),rargs,nargs)::s) ->
        let (rargs, nargs) = skip_native_args (m::rargs) nargs in
        begin match nargs with
          | [] ->
            let args = Array.of_list (List.rev rargs) in
-           begin match FredNative.red_prim (info_env info) () op args with
-             | Some m -> kni info tab m s
+           begin match FredNative.red_prim (info_env info) () op u args with
+             | Some m ->
+             kni info tab m s
              | None ->
                let f = {mark = mark Whnf KnownR; term = FFlex (ConstKey c)} in
                let m = {mark = mark Whnf KnownR; term = FApp(f,args)} in
@@ -1471,7 +1511,8 @@ and norm_head info tab m =
       | FProj (p,c) ->
           mkProj (p, kl info tab c)
       | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FConstruct _
-      | FApp _ | FCaseT _ | FCaseInvert _ | FLIFT _ | FCLOS _ | FInt _ | FFloat _ -> term_of_fconstr m
+      | FApp _ | FCaseT _ | FCaseInvert _ | FLIFT _ | FCLOS _ | FInt _
+      | FFloat _ | FArray _ -> term_of_fconstr m
 
 (* Initialization and then normalization *)
 
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index c1e5f12df7..ada0fc9780 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -118,6 +118,7 @@ type fterm =
   | FEvar of existential * fconstr subs
   | FInt of Uint63.t
   | FFloat of Float64.t
+  | FArray of Univ.Instance.t * fconstr Parray.t * fconstr
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs
   | FLOCKED
diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index c4036e9677..314cb54d1d 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -8,6 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Univ
+
 type t =
   | Int63head0
   | Int63tail0
@@ -51,6 +53,13 @@ type t =
   | Float64ldshiftexp
   | Float64next_up
   | Float64next_down
+  | Arraymake
+  | Arrayget
+  | Arraydefault
+  | Arrayset
+  | Arraycopy
+  | Arrayreroot
+  | Arraylength
 
 let parse = function
   | "int63_head0" -> Int63head0
@@ -95,6 +104,13 @@ let parse = function
   | "float64_ldshiftexp" -> Float64ldshiftexp
   | "float64_next_up" -> Float64next_up
   | "float64_next_down" -> Float64next_down
+  | "array_make" -> Arraymake
+  | "array_get" -> Arrayget
+  | "array_default" -> Arraydefault
+  | "array_set" -> Arrayset
+  | "array_length" -> Arraylength
+  | "array_copy" -> Arraycopy
+  | "array_reroot" -> Arrayreroot
   | _ -> raise Not_found
 
 let equal (p1 : t) (p2 : t) =
@@ -143,6 +159,13 @@ let hash = function
   | Float64eq -> 40
   | Float64lt -> 41
   | Float64le -> 42
+  | Arraymake -> 43
+  | Arrayget -> 44
+  | Arraydefault -> 45
+  | Arrayset -> 46
+  | Arraycopy -> 47
+  | Arrayreroot -> 48
+  | Arraylength -> 49
 
 (* Should match names in nativevalues.ml *)
 let to_string = function
@@ -188,28 +211,66 @@ let to_string = function
   | Float64ldshiftexp -> "ldshiftexp"
   | Float64next_up    -> "next_up"
   | Float64next_down  -> "next_down"
+  | Arraymake -> "arraymake"
+  | Arrayget -> "arrayget"
+  | Arraydefault -> "arraydefault"
+  | Arrayset -> "arrayset"
+  | Arraycopy -> "arraycopy"
+  | Arrayreroot -> "arrayreroot"
+  | Arraylength -> "arraylength"
+
+type const =
+  | Arraymaxlength
 
-type prim_type =
-  | PT_int63
-  | PT_float64
+let const_to_string = function
+  | Arraymaxlength -> "arraymaxlength"
+
+let const_of_string = function
+  | "array_max_length" -> Arraymaxlength
+  | _ -> raise Not_found
 
-type 'a prim_ind =
+let const_univs = function
+  | Arraymaxlength -> AUContext.empty
+
+type 'a prim_type =
+  | PT_int63 : unit prim_type
+  | PT_float64 : unit prim_type
+  | PT_array : (Instance.t * ind_or_type) prim_type
+
+and 'a prim_ind =
   | PIT_bool : unit prim_ind
-  | PIT_carry : prim_type prim_ind
-  | PIT_pair : (prim_type * prim_type) prim_ind
+  | PIT_carry : ind_or_type prim_ind
+  | PIT_pair : (ind_or_type * ind_or_type) prim_ind
   | PIT_cmp : unit prim_ind
   | PIT_f_cmp : unit prim_ind
   | PIT_f_class : unit prim_ind
 
-type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
-
-type ind_or_type =
+and ind_or_type =
   | PITT_ind : 'a prim_ind * 'a -> ind_or_type
-  | PITT_type : prim_type -> ind_or_type
+  | PITT_type : 'a prim_type * 'a -> ind_or_type
+  | PITT_param : int -> ind_or_type (* DeBruijn index referring to prenex type quantifiers *)
+
+let one_univ =
+  AUContext.make Names.[|Name (Id.of_string "u")|] Constraint.empty
+
+let typ_univs (type a) (t : a prim_type) = match t with
+  | PT_int63 -> AUContext.empty
+  | PT_float64 -> AUContext.empty
+  | PT_array -> one_univ
+
+type prim_type_ex = PTE : 'a prim_type -> prim_type_ex
+
+type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
 
 let types =
-  let int_ty = PITT_type PT_int63 in
-  let float_ty = PITT_type PT_float64 in
+  let int_ty = PITT_type (PT_int63, ()) in
+  let float_ty = PITT_type (PT_float64, ()) in
+  let array_ty =
+    PITT_type
+      (PT_array,
+       (Instance.of_array [|Level.var 0|],
+        PITT_param 1))
+  in
   function
   | Int63head0 | Int63tail0 -> [int_ty; int_ty]
   | Int63add | Int63sub | Int63mul
@@ -217,25 +278,144 @@ let types =
   | Int63lsr | Int63lsl
   | Int63land | Int63lor | Int63lxor -> [int_ty; int_ty; int_ty]
   | Int63addc | Int63subc | Int63addCarryC | Int63subCarryC ->
-     [int_ty; int_ty; PITT_ind (PIT_carry, PT_int63)]
+     [int_ty; int_ty; PITT_ind (PIT_carry, int_ty)]
   | Int63mulc | Int63diveucl ->
-     [int_ty; int_ty; PITT_ind (PIT_pair, (PT_int63, PT_int63))]
+     [int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))]
   | Int63eq | Int63lt | Int63le -> [int_ty; int_ty; PITT_ind (PIT_bool, ())]
   | Int63compare -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())]
   | Int63div21 ->
-     [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (PT_int63, PT_int63))]
+     [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))]
   | Int63addMulDiv -> [int_ty; int_ty; int_ty; int_ty]
   | Float64opp | Float64abs | Float64sqrt
   | Float64next_up | Float64next_down -> [float_ty; float_ty]
   | Float64ofInt63 -> [int_ty; float_ty]
   | Float64normfr_mantissa -> [float_ty; int_ty]
-  | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (PT_float64, PT_int63))]
+  | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (float_ty, int_ty))]
   | Float64eq | Float64lt | Float64le -> [float_ty; float_ty; PITT_ind (PIT_bool, ())]
   | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_f_cmp, ())]
   | Float64classify -> [float_ty; PITT_ind (PIT_f_class, ())]
   | Float64add | Float64sub | Float64mul
   | Float64div -> [float_ty; float_ty; float_ty]
   | Float64ldshiftexp -> [float_ty; int_ty; float_ty]
+  | Arraymake -> [int_ty; PITT_param 1; array_ty]
+  | Arrayget -> [array_ty; int_ty; PITT_param 1]
+  | 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 =
+  (* currently if there's a parameter it's always this *)
+  let a_annot = Context.nameR (Names.Id.of_string "A") in
+  let ty = Constr.mkType (Universe.make (Level.var 0)) in
+  Context.Rel.Declaration.[LocalAssum (a_annot, ty)]
+
+let params = function
+  | Int63head0
+  | Int63tail0
+  | Int63add
+  | Int63sub
+  | Int63mul
+  | Int63div
+  | Int63mod
+  | Int63lsr
+  | Int63lsl
+  | Int63land
+  | Int63lor
+  | Int63lxor
+  | Int63addc
+  | Int63subc
+  | Int63addCarryC
+  | Int63subCarryC
+  | Int63mulc
+  | Int63diveucl
+  | Int63div21
+  | Int63addMulDiv
+  | Int63eq
+  | Int63lt
+  | Int63le
+  | Int63compare
+  | Float64opp
+  | Float64abs
+  | Float64eq
+  | Float64lt
+  | Float64le
+  | Float64compare
+  | Float64classify
+  | Float64add
+  | Float64sub
+  | Float64mul
+  | Float64div
+  | Float64sqrt
+  | Float64ofInt63
+  | Float64normfr_mantissa
+  | Float64frshiftexp
+  | Float64ldshiftexp
+  | Float64next_up
+  | Float64next_down -> []
+
+  | Arraymake
+  | Arrayget
+  | Arraydefault
+  | Arrayset
+  | Arraycopy
+  | Arrayreroot
+  | Arraylength -> one_param
+
+let nparams x = List.length (params x)
+
+let univs = function
+  | Int63head0
+  | Int63tail0
+  | Int63add
+  | Int63sub
+  | Int63mul
+  | Int63div
+  | Int63mod
+  | Int63lsr
+  | Int63lsl
+  | Int63land
+  | Int63lor
+  | Int63lxor
+  | Int63addc
+  | Int63subc
+  | Int63addCarryC
+  | Int63subCarryC
+  | Int63mulc
+  | Int63diveucl
+  | Int63div21
+  | Int63addMulDiv
+  | Int63eq
+  | Int63lt
+  | Int63le
+  | Int63compare
+  | Float64opp
+  | Float64abs
+  | Float64eq
+  | Float64lt
+  | Float64le
+  | Float64compare
+  | Float64classify
+  | Float64add
+  | Float64sub
+  | Float64mul
+  | Float64div
+  | Float64sqrt
+  | Float64ofInt63
+  | Float64normfr_mantissa
+  | Float64frshiftexp
+  | Float64ldshiftexp
+  | Float64next_up
+  | Float64next_down -> AUContext.empty
+
+  | Arraymake
+  | Arrayget
+  | Arraydefault
+  | Arrayset
+  | Arraycopy
+  | Arrayreroot
+  | Arraylength -> one_univ
 
 type arg_kind =
   | Kparam (* not needed for the evaluation of the primitive when it reduces *)
@@ -247,17 +427,21 @@ type args_red = arg_kind list
 (* Invariant only argument of type int63, float or an inductive can
    have kind Kwhnf *)
 
-let arity t = List.length (types t) - 1
+let arity t = let sign = types t in nparams t + List.length sign - 1
 
 let kind t =
-  let rec aux n = if n <= 0 then [] else Kwhnf :: aux (n - 1) in
-  aux (arity t)
+  let rec params n = if n <= 0 then [] else Kparam :: params (n - 1) in
+  let args = function PITT_type _ | PITT_ind _ -> Kwhnf | PITT_param _ -> Karg in
+  params (nparams t) @ List.map args (CList.drop_last (types t))
+
+let types t = params t, types t
 
 (** Special Entries for Register **)
 
 type op_or_type =
   | OT_op of t
-  | OT_type of prim_type
+  | OT_type : 'a prim_type -> op_or_type
+  | OT_const of const
 
 let prim_ind_to_string (type a) (p : a prim_ind) = match p with
   | PIT_bool -> "bool"
@@ -267,24 +451,40 @@ let prim_ind_to_string (type a) (p : a prim_ind) = match p with
   | PIT_f_cmp -> "f_cmp"
   | PIT_f_class -> "f_class"
 
-let prim_type_to_string = function
+let prim_type_to_string (type a) (ty : a prim_type) = match ty with
   | PT_int63 -> "int63_type"
   | PT_float64 -> "float64_type"
+  | PT_array -> "array_type"
 
 let op_or_type_to_string = function
   | OT_op op -> to_string op
   | OT_type t -> prim_type_to_string t
+  | OT_const c -> const_to_string c
 
 let prim_type_of_string = function
-  | "int63_type" -> PT_int63
-  | "float64_type" -> PT_float64
+  | "int63_type" -> PTE PT_int63
+  | "float64_type" -> PTE PT_float64
+  | "array_type" -> PTE PT_array
   | _ -> raise Not_found
 
 let op_or_type_of_string s =
-  try OT_type (prim_type_of_string s)
-  with Not_found -> OT_op (parse s)
+  match prim_type_of_string s with
+  | PTE ty -> OT_type ty
+  | exception Not_found ->
+    begin try OT_op (parse s)
+      with Not_found -> OT_const (const_of_string s)
+    end
 
 let parse_op_or_type ?loc s =
   try op_or_type_of_string s
   with Not_found ->
     CErrors.user_err ?loc Pp.(str ("Built-in #"^s^" does not exist."))
+
+let op_or_type_univs = function
+  | OT_op t -> univs t
+  | OT_type t -> typ_univs t
+  | OT_const c -> const_univs c
+
+let body_of_prim_const = function
+  | Arraymaxlength ->
+    Constr.mkInt (Parray.max_length)
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli
index a5db51111f..5e5fad9f04 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -51,6 +51,13 @@ type t =
   | Float64ldshiftexp
   | Float64next_up
   | Float64next_down
+  | Arraymake
+  | Arrayget
+  | Arraydefault
+  | Arrayset
+  | Arraycopy
+  | Arrayreroot
+  | Arraylength
 
 (** Can raise [Not_found].
     Beware that this is not exactly the reverse of [to_string] below. *)
@@ -58,8 +65,11 @@ val parse : string -> t
 
 val equal : t -> t -> bool
 
+type const =
+  | Arraymaxlength
+
 type arg_kind =
-  | Kparam (* not needed for the elavuation of the primitive*)
+  | Kparam (* not needed for the evaluation of the primitive*)
   | Kwhnf  (* need to be reduced in whnf before reducing the primitive *)
   | Karg   (* no need to be reduced in whnf *)
 
@@ -70,32 +80,49 @@ val hash : t -> int
 val to_string : t -> string
 
 val arity : t -> int
+(** Including parameters *)
+
+val nparams : t -> int
 
 val kind : t -> args_red
+(** Includes parameters *)
 
 (** Special Entries for Register **)
 
-type prim_type =
-  | PT_int63
-  | PT_float64
-
-(** Can raise [Not_found] *)
-val prim_type_of_string : string -> prim_type
-val prim_type_to_string : prim_type -> string
+type 'a prim_type =
+  | PT_int63 : unit prim_type
+  | PT_float64 : unit prim_type
+  | PT_array : (Univ.Instance.t * ind_or_type) prim_type
 
-type 'a prim_ind =
+and 'a prim_ind =
   | PIT_bool : unit prim_ind
-  | PIT_carry : prim_type prim_ind
-  | PIT_pair : (prim_type * prim_type) prim_ind
+  | PIT_carry : ind_or_type prim_ind
+  | PIT_pair : (ind_or_type * ind_or_type) prim_ind
   | PIT_cmp : unit prim_ind
   | PIT_f_cmp : unit prim_ind
   | PIT_f_class : unit prim_ind
 
+and ind_or_type =
+  | PITT_ind : 'a prim_ind * 'a -> ind_or_type
+  | PITT_type : 'a prim_type * 'a -> ind_or_type
+  | PITT_param : int -> ind_or_type (* DeBruijn index referring to prenex type quantifiers *)
+
+val typ_univs : 'a prim_type -> Univ.AUContext.t
+
+type prim_type_ex = PTE : 'a prim_type -> prim_type_ex
+
 type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
 
+(** Can raise [Not_found] *)
+val prim_type_of_string : string -> prim_type_ex
+val prim_type_to_string : 'a prim_type -> string
+
 type op_or_type =
   | OT_op of t
-  | OT_type of prim_type
+  | OT_type : 'a prim_type -> op_or_type
+  | OT_const of const
+
+val op_or_type_univs : op_or_type -> Univ.AUContext.t
 
 val prim_ind_to_string : 'a prim_ind -> string
 
@@ -105,8 +132,12 @@ val op_or_type_to_string : op_or_type -> string
 
 val parse_op_or_type : ?loc:Loc.t -> string -> op_or_type
 
-type ind_or_type =
-  | PITT_ind : 'a prim_ind * 'a -> ind_or_type
-  | PITT_type : prim_type -> ind_or_type
+val univs : t -> Univ.AUContext.t
+
+val types : t -> Constr.rel_context * ind_or_type list
+(** Parameters * Reduction relevant arguments and output type
+
+  XXX we could reify universes in ind_or_type (currently polymorphic types
+  like array are assumed to use universe 0). *)
 
-val types : t -> ind_or_type list
+val body_of_prim_const : const -> Constr.t
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 25ec250367..74405a0105 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -61,6 +61,7 @@ type instruction =
   | Kensurestackcapacity of int
   | Kbranch of Label.t                  (* jump to label *)
   | Kprim of CPrimitives.t * pconstant option
+  | Kcamlprim of CPrimitives.t * Label.t
   | Kareint of int
 
 and bytecodes = instruction list
@@ -147,6 +148,10 @@ let rec pp_instr i =
   | Kprim (op, id) -> str (CPrimitives.to_string op) ++ str " " ++
         (match id with Some (id,_u) -> Constant.print id | None -> str "")
 
+  | Kcamlprim (op, lbl) ->
+    str "camlcall " ++ str (CPrimitives.to_string op) ++ spc () ++
+    pp_lbl lbl
+
   | Kareint n -> str "areint " ++ int n
 
 and pp_bytecodes c =
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index f1d441ca76..b703058fb7 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -60,7 +60,7 @@ type instruction =
 
   | Kbranch of Label.t                  (** jump to label, is it needed ? *)
   | Kprim of CPrimitives.t * pconstant option
-
+  | Kcamlprim of CPrimitives.t * Label.t
   | Kareint of int
 
 and bytecodes = instruction list
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 59ae8c0745..7bff377238 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -516,6 +516,18 @@ let rec get_alias env kn =
         | BCalias kn' -> get_alias env kn'
         | _ -> kn)
 
+(* Some primitives are not implemented natively by the VM, but calling OCaml
+   code instead *)
+let is_caml_prim = let open CPrimitives in function
+  | Arraymake
+  | Arrayget
+  | Arraydefault
+  | Arrayset
+  | Arraycopy
+  | Arrayreroot
+  | Arraylength -> true
+  | _ -> false
+
 (* sz is the size of the local stack *)
 let rec compile_lam env cenv lam sz cont =
   set_max_stack_size sz;
@@ -775,6 +787,27 @@ let rec compile_lam env cenv lam sz cont =
     let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in
     comp_args (compile_lam env) cenv args sz cont
 
+  | Lprim (Some (kn,u), op, args) when is_caml_prim op ->
+    let arity = CPrimitives.arity op in
+    let nparams = CPrimitives.nparams op in
+    let nargs = arity - nparams in
+    assert (arity = Array.length args && arity <= 4);
+    let (jump, cont) = make_branch cont in
+    let lbl_default = Label.create () in
+    let default =
+      let cont = [Kgetglobal kn; Kapply (arity + Univ.Instance.length u); jump] in
+      let cont =
+        if Univ.Instance.is_empty u then cont
+        else comp_args compile_universe cenv (Univ.Instance.to_array u) (sz + arity) (Kpush::cont)
+      in
+      Klabel lbl_default ::
+      Kpush ::
+      if Int.equal nparams 0 then cont
+      else comp_args (compile_lam env) cenv (Array.sub args 0 nparams) (sz + nargs) (Kpush::cont)
+    in
+    fun_code := [Ksequence(default, !fun_code)];
+    comp_args (compile_lam env) cenv (Array.sub args nparams nargs) sz (Kcamlprim (op, lbl_default) :: cont)
+
   | Lprim (kn, op, args) ->
     comp_args (compile_lam env) cenv args sz (Kprim(op, kn)::cont)
 
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index d855dbf2bb..6b4daabf0c 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -30,6 +30,7 @@ type reloc_info =
   | Reloc_const of structured_constant
   | Reloc_getglobal of Names.Constant.t
   | Reloc_proj_name of Projection.Repr.t
+  | Reloc_caml_prim of CPrimitives.t
 
 let eq_reloc_info r1 r2 = match r1, r2 with
 | Reloc_annot sw1, Reloc_annot sw2 -> eq_annot_switch sw1 sw2
@@ -40,6 +41,8 @@ let eq_reloc_info r1 r2 = match r1, r2 with
 | Reloc_getglobal _, _ -> false
 | Reloc_proj_name p1, Reloc_proj_name p2 -> Projection.Repr.equal p1 p2
 | Reloc_proj_name _, _ -> false
+| Reloc_caml_prim p1, Reloc_caml_prim p2 -> CPrimitives.equal p1 p2
+| Reloc_caml_prim _, _ -> false
 
 let hash_reloc_info r =
   let open Hashset.Combine in
@@ -48,6 +51,7 @@ let hash_reloc_info r =
   | Reloc_const c -> combinesmall 2 (hash_structured_constant c)
   | Reloc_getglobal c -> combinesmall 3 (Constant.hash c)
   | Reloc_proj_name p -> combinesmall 4 (Projection.Repr.hash p)
+  | Reloc_caml_prim p -> combinesmall 5 (CPrimitives.hash p)
 
 module RelocTable = Hashtbl.Make(struct
   type t = reloc_info
@@ -199,6 +203,10 @@ let slot_for_proj_name env p =
   enter env (Reloc_proj_name p);
   out_int env 0
 
+let slot_for_caml_prim env op =
+  enter env (Reloc_caml_prim op);
+  out_int env 0
+
 (* Emission of one instruction *)
 
 let nocheck_prim_op = function
@@ -252,6 +260,11 @@ let check_prim_op = function
   | Float64ldshiftexp -> opCHECKLDSHIFTEXP
   | Float64next_up    -> opCHECKNEXTUPFLOAT
   | Float64next_down  -> opCHECKNEXTDOWNFLOAT
+  | Arraymake -> opISINT_CAML_CALL2
+  | Arrayget -> opISARRAY_INT_CAML_CALL2
+  | Arrayset -> opISARRAY_INT_CAML_CALL3
+  | Arraydefault | Arraycopy | Arrayreroot | Arraylength ->
+      opISARRAY_CAML_CALL1
 
 let emit_instr env = function
   | Klabel lbl -> define_label env lbl
@@ -349,6 +362,11 @@ let emit_instr env = function
       out env (check_prim_op op);
       slot_for_getglobal env q
 
+  | Kcamlprim (op,lbl) ->
+    out env (check_prim_op op);
+    out_label env lbl;
+    slot_for_caml_prim env op
+
   | Kareint 1 -> out env opISINT
   | Kareint 2 -> out env opAREINT2;
 
@@ -415,6 +433,7 @@ let subst_reloc s ri =
   | Reloc_const sc -> Reloc_const (subst_strcst s sc)
   | Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn)
   | Reloc_proj_name p -> Reloc_proj_name (subst_proj_repr s p)
+  | Reloc_caml_prim _ -> ri
 
 let subst_patches subst p =
   let infos = CArray.map (fun (r, pos) -> (subst_reloc subst r, pos)) p.reloc_infos in
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index 209d741ba8..c4262f3380 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -16,6 +16,7 @@ type reloc_info =
   | Reloc_const of structured_constant
   | Reloc_getglobal of Constant.t
   | Reloc_proj_name of Projection.Repr.t
+  | Reloc_caml_prim of CPrimitives.t
 
 type patches
 type emitcodes
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 0d77cae077..6690a379ce 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -542,6 +542,14 @@ let makeblock tag nparams arity args =
       Lval(val_of_block Obj.last_non_constant_constructor_tag args)
   else Lmakeblock(tag, args)
 
+let makearray args def =
+  try
+    let p = Array.map get_value args in
+    Lval (val_of_parray @@ Parray.unsafe_of_array p (get_value def))
+  with Not_found ->
+    let ar = Lmakeblock(0, args) in (* build the ocaml array *)
+    let kind = Lmakeblock(0, [|ar; def|]) in (* Parray.Array *)
+    Lmakeblock(0,[|kind|]) (* the reference *)
 
 (* Compiling constants *)
 
@@ -568,8 +576,13 @@ let expand_prim kn op arity =
 
 let lambda_of_prim kn op args =
   let arity = CPrimitives.arity op in
-  if Array.length args >= arity then prim kn op args
-  else mkLapp (expand_prim kn op arity) args
+  match Int.compare (Array.length args) arity with
+  | 0 -> prim kn op args
+  | x when x > 0 ->
+    let prim_args = Array.sub args 0 arity in
+    let extra_args = Array.sub args arity (Array.length args - arity) in
+    mkLapp(prim kn op prim_args) extra_args
+  | _ -> mkLapp (expand_prim kn op arity) args
 
 (*i Global environment *)
 
@@ -768,6 +781,9 @@ let rec lambda_of_constr env c =
 
   | Int i -> Luint i
   | Float f -> Lfloat f
+  | Array(_u, t,def,_ty) ->
+    let def = lambda_of_constr env def in
+    makearray (lambda_of_args env 0 t) def
 
 and lambda_of_app env f args =
   match Constr.kind f with
diff --git a/kernel/constr.ml b/kernel/constr.ml
index d0598bdad1..1837a39764 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -109,6 +109,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Proj      of Projection.t * 'constr
   | Int       of Uint63.t
   | Float     of Float64.t
+  | Array     of 'univs * 'constr array * 'constr * 'types
 (* constr is the fixpoint of the previous type. Requires option
    -rectypes of the Caml compiler to be set *)
 type t = (t, t, Sorts.t, Instance.t) kind_of_term
@@ -246,6 +247,9 @@ let mkRef (gr,u) = let open GlobRef in match gr with
 (* Constructs a primitive integer *)
 let mkInt i = Int i
 
+(* Constructs an array *)
+let mkArray (u,t,def,ty) = Array (u,t,def,ty)
+
 (* Constructs a primitive float number *)
 let mkFloat f = Float f
 
@@ -485,6 +489,8 @@ let fold f acc c = match kind c with
     Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
   | CoFix (_,(_lna,tl,bl)) ->
     Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
+  | Array(_u,t,def,ty) ->
+    f (f (Array.fold_left f acc t) def) ty
 
 (* [iter f c] iters [f] on the immediate subterms of [c]; it is
    not recursive and the order with which subterms are processed is
@@ -508,6 +514,7 @@ let iter f c = match kind c with
   | Case (_,p,iv,c,bl) -> f p; iter_invert f iv; f c; Array.iter f bl
   | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
   | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
+  | Array(_u,t,def,ty) -> Array.iter f t; f def; f ty
 
 (* [iter_with_binders g f n c] iters [f n] on the immediate
    subterms of [c]; it carries an extra data [n] (typically a lift
@@ -532,6 +539,8 @@ let iter_with_binders g f n c = match kind c with
   | CoFix (_,(_,tl,bl)) ->
       Array.Fun1.iter f n tl;
       Array.Fun1.iter f (iterate g (Array.length tl) n) bl
+  | Array(_u,t,def,ty) ->
+    Array.iter (f n) t; f n def; f n ty
 
 (* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
    subterms of [c] starting from [acc] and proceeding from left to
@@ -560,6 +569,8 @@ let fold_constr_with_binders g f n acc c =
       let n' = iterate g (Array.length tl) n in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+  | Array(_u,t,def,ty) ->
+    f n (f n (Array.fold_left (f n) acc t) def) ty
 
 (* [map f c] maps [f] on the immediate subterms of [c]; it is
    not recursive and the order with which subterms are processed is
@@ -705,6 +716,12 @@ let map_gen userview f c = match kind c with
       let bl' = Array.Smart.map f bl in
       if tl'==tl && bl'==bl then c
       else mkCoFix (ln,(lna,tl',bl'))
+  | Array(u,t,def,ty) ->
+    let t' = Array.Smart.map f t in
+    let def' = f def in
+    let ty' = f ty in
+    if def'==def && t==t' && ty==ty' then c
+    else mkArray(u,t',def',ty')
 
 let map_user_view = map_gen true
 let map = map_gen false
@@ -773,6 +790,12 @@ let fold_map f accu c = match kind c with
       let accu, bl' = Array.Smart.fold_left_map f accu bl in
       if tl'==tl && bl'==bl then accu, c
       else accu, mkCoFix (ln,(lna,tl',bl'))
+  | Array(u,t,def,ty) ->
+    let accu, t' = Array.Smart.fold_left_map f accu t in
+    let accu, def' = f accu def in
+    let accu, ty' = f accu ty in
+    if def'==def && t==t' && ty==ty' then accu, c
+    else accu, mkArray(u,t',def',ty')
 
 (* [map_with_binders g f n c] maps [f n] on the immediate
    subterms of [c]; it carries an extra data [n] (typically a lift
@@ -835,6 +858,12 @@ let map_with_binders g f l c0 = match kind c0 with
     let l' = iterate g (Array.length tl) l in
     let bl' = Array.Fun1.Smart.map f l' bl in
     mkCoFix (ln,(lna,tl',bl'))
+  | Array(u,t,def,ty) ->
+    let t' = Array.Fun1.Smart.map f l t in
+    let def' = f l def in
+    let ty' = f l ty in
+    if def'==def && t==t' && ty==ty' then c0
+    else mkArray(u,t',def',ty')
 
 (*********************)
 (*      Lifting      *)
@@ -877,6 +906,7 @@ let fold_with_full_binders g f n acc c =
       let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+  | Array(_u,t,def,ty) -> f n (f n (Array.fold_left (f n) acc t) def) ty
 
 
 type 'univs instance_compare_fn = (GlobRef.t * int) option ->
@@ -935,9 +965,13 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
     && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2
   | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
     Int.equal ln1 ln2 && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2
+  | Array(u1,t1,def1,ty1), Array(u2,t2,def2,ty2) ->
+    leq_universes None u1 u2 &&
+    Array.equal_norefl (eq 0) t1 t2 &&
+    eq 0 def1 def2 && eq 0 ty1 ty2
   | (Rel _ | Meta _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _
     | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _
-    | CoFix _ | Int _ | Float _), _ -> false
+    | CoFix _ | Int _ | Float _| Array _), _ -> false
 
 (* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare
    the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity,
@@ -1129,6 +1163,9 @@ let constr_ord_int f t1 t2 =
     | Int i1, Int i2 -> Uint63.compare i1 i2
     | Int _, _ -> -1 | _, Int _ -> 1
     | Float f1, Float f2 -> Float64.total_compare f1 f2
+    | Array(_u1,t1,def1,ty1), Array(_u2,t2,def2,ty2) ->
+      (((Array.compare f) =? f) ==? f) t1 t2 def1 def2 ty1 ty2
+    | Array _, _ -> -1 | _, Array _ -> 1
 
 let rec compare m n=
   constr_ord_int compare m n
@@ -1222,9 +1259,11 @@ let hasheq t1 t2 =
       && array_eqeq bl1 bl2
     | Int i1, Int i2 -> i1 == i2
     | Float f1, Float f2 -> Float64.equal f1 f2
+    | Array(u1,t1,def1,ty1), Array(u2,t2,def2,ty2) ->
+      u1 == u2 && def1 == def2 && ty1 == ty2 && array_eqeq t1 t2
     | (Rel _ | Meta _ | Var _ | Sort _ | Cast _ | Prod _ | Lambda _ | LetIn _
       | App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _
-      | Fix _ | CoFix _ | Int _ | Float _), _ -> false
+      | Fix _ | CoFix _ | Int _ | Float _ | Array _), _ -> false
 
 (** Note that the following Make has the side effect of creating
     once and for all the table we'll use for hash-consing all constr *)
@@ -1332,6 +1371,13 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
         let (h,l) = Uint63.to_int2 i in
         (t, combinesmall 18 (combine h l))
       | Float f -> (t, combinesmall 19 (Float64.hash f))
+      | Array (u,t,def,ty) ->
+        let u, hu = sh_instance u in
+        let t, ht = hash_term_array t in
+        let def, hdef = sh_rec def in
+        let ty, hty = sh_rec ty in
+        let h = combine4 hu ht hdef hty in
+        (Array(u,t,def,ty), combinesmall 20 h)
 
   and sh_invert = function
     | NoInvert -> NoInvert, 0
@@ -1413,6 +1459,8 @@ let rec hash t =
       combinesmall 17 (combine (Projection.hash p) (hash c))
     | Int i -> combinesmall 18 (Uint63.hash i)
     | Float f -> combinesmall 19 (Float64.hash f)
+    | Array(u,t,def,ty) ->
+      combinesmall 20 (combine4 (Instance.hash u) (hash_term_array t) (hash def) (hash ty))
 
 and hash_invert = function
   | NoInvert -> 0
@@ -1566,6 +1614,9 @@ let rec debug_print c =
          str"}")
   | Int i -> str"Int("++str (Uint63.to_string i) ++ str")"
   | Float i -> str"Float("++str (Float64.to_string i) ++ str")"
+  | Array(u,t,def,ty) -> str"Array(" ++ prlist_with_sep pr_comma debug_print (Array.to_list t) ++ str" | "
+      ++ debug_print def ++ str " : " ++ debug_print ty
+      ++ str")@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str"}"
 
 and debug_invert = let open Pp in function
   | NoInvert -> mt()
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 0c151bb43c..62f2555a7e 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -84,6 +84,9 @@ val mkVar : Id.t -> constr
 (** Constructs a machine integer *)
 val mkInt : Uint63.t -> constr
 
+(** Constructs an array *)
+val mkArray : Univ.Instance.t * constr array * constr * types -> constr
+
 (** Constructs a machine float number *)
 val mkFloat : Float64.t -> constr
 
@@ -246,6 +249,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Proj      of Projection.t * 'constr
   | Int       of Uint63.t
   | Float     of Float64.t
+  | Array     of 'univs * 'constr array * 'constr * 'types
 
 (** User view of [constr]. For [App], it is ensured there is at
    least one argument and the function is not itself an applicative
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index f41585e93a..185fb9f5a4 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -63,6 +63,15 @@ let set_global v =
   global_data.glob_len <- global_data.glob_len + 1;
   n
 
+(* Initialization of OCaml primitives *)
+let parray_make = set_global Vmvalues.parray_make
+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 *)
 
 module SConstTable = Hashtbl.Make (struct
@@ -119,6 +128,17 @@ let slot_for_annot key =
     AnnotTable.add annot_tbl key n;
     n
 
+let slot_for_caml_prim =
+  let open CPrimitives in function
+  | Arraymake -> parray_make
+  | Arrayget -> parray_get
+  | Arraydefault -> parray_get_default
+  | Arrayset -> parray_set
+  | Arraycopy -> parray_copy
+  | Arrayreroot -> parray_reroot
+  | Arraylength -> parray_length
+  | _ -> assert false
+
 let slot_for_proj_name key =
   try ProjNameTable.find proj_name_tbl key
   with Not_found ->
@@ -182,6 +202,7 @@ and eval_to_patch env (buff,pl,fv) =
     | Reloc_const sc -> slot_for_str_cst sc
     | Reloc_getglobal kn -> slot_for_getglobal env kn
     | Reloc_proj_name p -> slot_for_proj_name p
+    | Reloc_caml_prim op -> slot_for_caml_prim op
   in
   let tc = patch buff pl slots in
   let vm_env =
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 68bd1cbac9..7609c1a64d 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -55,7 +55,7 @@ type ('a, 'opaque) constant_def =
   | Undef of inline                       (** a global assumption *)
   | Def of 'a                             (** or a transparent global definition *)
   | OpaqueDef of 'opaque                  (** or an opaque global definition *)
-  | Primitive of CPrimitives.t            (** or a primitive operation *)
+  | Primitive of CPrimitives.t (** or a primitive operation *)
 
 type universes =
   | Monomorphic of Univ.ContextSet.t
@@ -116,11 +116,14 @@ type 'opaque constant_body = {
 }
 
 (** {6 Representation of mutual inductive types in the kernel } *)
+type nested_type =
+| NestedInd of inductive
+| NestedPrimitive of Constant.t
 
 type recarg =
-  | Norec
-  | Mrec of inductive
-  | Imbr of inductive
+| Norec
+| Mrec of inductive
+| Nested of nested_type
 
 type wf_paths = recarg Rtree.t
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 3de2cb00a4..326bf0d6ad 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -156,21 +156,47 @@ let hcons_const_body cb =
   }
 
 (** {6 Inductive types } *)
+let eq_nested_type t1 t2 = match t1, t2 with
+| NestedInd ind1, NestedInd ind2 -> Names.eq_ind ind1 ind2
+| NestedInd _, _ -> false
+| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.equal c1 c2
+| NestedPrimitive _, _ -> false
 
 let eq_recarg r1 r2 = match r1, r2 with
 | Norec, Norec -> true
+| Norec, _ -> false
 | Mrec i1, Mrec i2 -> Names.eq_ind i1 i2
-| Imbr i1, Imbr i2 -> Names.eq_ind i1 i2
-| _ -> false
+| Mrec _, _ -> false
+| Nested ty1, Nested ty2 -> eq_nested_type ty1 ty2
+| Nested _, _ -> false
+
+let pp_recarg = let open Pp in function
+  | Declarations.Norec -> str "Norec"
+  | Declarations.Mrec (mind,i) ->
+     str "Mrec[" ++ Names.MutInd.print mind ++ pr_comma () ++ int i ++ str "]"
+  | Declarations.(Nested (NestedInd (mind,i))) ->
+     str "Nested[" ++ Names.MutInd.print mind ++ pr_comma () ++ int i ++ str "]"
+  | Declarations.(Nested (NestedPrimitive c)) ->
+     str "Nested[" ++ Names.Constant.print c ++ str "]"
+
+let pp_wf_paths x = Rtree.pp_tree pp_recarg x
+
+let subst_nested_type sub ty = match ty with
+| NestedInd (kn,i) ->
+  let kn' = subst_mind sub kn in
+  if kn==kn' then ty else NestedInd (kn',i)
+| NestedPrimitive c ->
+  let c',_ = subst_con sub c in
+  if c==c' then ty else NestedPrimitive c'
 
 let subst_recarg sub r = match r with
   | Norec -> r
   | Mrec (kn,i) ->
     let kn' = subst_mind sub kn in
     if kn==kn' then r else Mrec (kn',i)
-  | Imbr (kn,i) ->
-    let kn' = subst_mind sub kn in
-    if kn==kn' then r else Imbr (kn',i)
+  | Nested ty ->
+    let ty' = subst_nested_type sub ty in
+    if ty==ty' then r else Nested ty'
 
 let mk_norec = Rtree.mk_node Norec [||]
 
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 01e4429e7e..4ab8d45e60 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -46,6 +46,9 @@ val is_opaque : 'a constant_body -> bool
 
 val eq_recarg : recarg -> recarg -> bool
 
+val pp_recarg : recarg -> Pp.t
+val pp_wf_paths : wf_paths -> Pp.t
+
 val subst_recarg : substitution -> recarg -> recarg
 
 val mk_norec : wf_paths
diff --git a/kernel/entries.ml b/kernel/entries.ml
index e0b678621a..ae64112e33 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -91,8 +91,7 @@ type parameter_entry =
     Id.Set.t option * types in_universes_entry * inline
 
 type primitive_entry = {
-  prim_entry_type : types option;
-  prim_entry_univs : Univ.ContextSet.t; (* always monomorphic *)
+  prim_entry_type : types in_universes_entry option;
   prim_entry_content : CPrimitives.op_or_type;
 }
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 0ae6f242f6..e75ccbb252 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -503,7 +503,7 @@ let constant_type env (kn,u) =
 type const_evaluation_result =
   | NoBody
   | Opaque
-  | IsPrimitive of CPrimitives.t
+  | IsPrimitive of Univ.Instance.t * CPrimitives.t
 
 exception NotEvaluableConst of const_evaluation_result
 
@@ -535,7 +535,7 @@ let constant_value_in env (kn,u) =
         subst_instance_constr u b
     | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
     | Undef _ -> raise (NotEvaluableConst NoBody)
-    | Primitive p -> raise (NotEvaluableConst (IsPrimitive p))
+    | Primitive p -> raise (NotEvaluableConst (IsPrimitive (u,p)))
 
 let constant_opt_value_in env cst =
   try Some (constant_value_in env cst)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f489b13a3b..5cb56a2a29 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -225,7 +225,7 @@ val type_in_type_constant : Constant.t -> env -> bool
 type const_evaluation_result =
   | NoBody
   | Opaque
-  | IsPrimitive of CPrimitives.t
+  | IsPrimitive of Univ.Instance.t * CPrimitives.t
 exception NotEvaluableConst of const_evaluation_result
 
 val constant_type : env -> Constant.t puniverses -> types constrained
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index 0a9f137c45..67a672c349 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -157,6 +157,10 @@ let opcodes =
     "CHECKLDSHIFTEXP";
     "CHECKNEXTUPFLOAT";
     "CHECKNEXTDOWNFLOAT";
+    "ISINT_CAML_CALL2";
+    "ISARRAY_CAML_CALL1";
+    "ISARRAY_INT_CAML_CALL2";
+    "ISARRAY_INT_CAML_CALL3";
     "STOP"
   |]
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 9da6c7842e..a27ff41a1c 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -165,7 +165,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) =
     let decl = LocalAssum (anon, hnf_prod_applist env ty lrecparams) in
     push_rel decl env in
   let ra_env' =
-    (Imbr mi,(Rtree.mk_rec_calls 1).(0)) ::
+    (Nested (NestedInd mi),(Rtree.mk_rec_calls 1).(0)) ::
     List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
   (* New index of the inductive types *)
   let newidx = n + auxntyp in
@@ -241,6 +241,9 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
                 discharged to the [check_positive_nested] function. *)
             if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec)
             else check_positive_nested ienv nmr (ind_kn, largs)
+        | Const (c,_) when is_primitive_positive_container env c ->
+          if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec)
+          else check_positive_nested_primitive ienv nmr (c, largs)
         | _err ->
             (** If an inductive of the mutually inductive block
                 appears in any other way, then the positivy check gives
@@ -298,7 +301,16 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
         let irecargs = Array.map snd irecargs_nmr
         and nmr' = array_min nmr irecargs_nmr
         in
-          (nmr',(Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0))
+          (nmr',(Rtree.mk_rec [|mk_paths (Nested (NestedInd mi)) irecargs|]).(0))
+
+  and check_positive_nested_primitive (env,n,ntypes,ra_env) nmr (c, largs) =
+    (* We model the primitive type c X1 ... Xn as if it had one constructor
+       C : X1 -> ... -> Xn -> c X1 ... Xn
+       The subterm relation is defined for each primitive in `inductive.ml`. *)
+    let ra_env = List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
+    let ienv = (env,n,ntypes,ra_env) in
+    let nmr',recargs = List.fold_left_map (check_pos ienv) nmr largs in
+    (nmr', (Rtree.mk_rec [| mk_paths (Nested (NestedPrimitive c)) [| recargs |] |]).(0))
 
   (** [check_constructors ienv check_head nmr c] checks the positivity
       condition in the type [c] of a constructor (i.e. that recursive
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index c51d82ce07..d751d9875a 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -464,11 +464,16 @@ let eq_wf_paths = Rtree.equal Declareops.eq_recarg
 
 let inter_recarg r1 r2 = match r1, r2 with
 | Norec, Norec -> Some r1
+| Norec, _ -> None
 | Mrec i1, Mrec i2
-| Imbr i1, Imbr i2
-| Mrec i1, Imbr i2 -> if Names.eq_ind i1 i2 then Some r1 else None
-| Imbr i1, Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None
-| _ -> None
+| Nested (NestedInd i1), Nested (NestedInd i2)
+| Mrec i1, (Nested (NestedInd i2)) -> if Names.eq_ind i1 i2 then Some r1 else None
+| Mrec _, _ -> None
+| Nested (NestedInd i1), Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None
+| Nested (NestedInd _), _ -> None
+| Nested (NestedPrimitive c1), Nested (NestedPrimitive c2) ->
+  if Names.Constant.equal c1 c2 then Some r1 else None
+| Nested (NestedPrimitive _), _ -> None
 
 let inter_wf_paths = Rtree.inter Declareops.eq_recarg inter_recarg Norec
 
@@ -551,8 +556,8 @@ let lookup_subterms env ind =
 
 let match_inductive ind ra =
   match ra with
-    | (Mrec i | Imbr i) -> eq_ind ind i
-    | Norec -> false
+    | Mrec i | Nested (NestedInd i) -> eq_ind ind i
+    | Norec | Nested (NestedPrimitive _) -> false
 
 (* In {match c as z in ci y_s return P with |C_i x_s => t end}
    [branches_specif renv c_spec ci] returns an array of x_s specs knowing
@@ -603,7 +608,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
     push_rel decl env
   in
   let env = Array.fold_right push_ind mib.mind_packets env in
-  let rc = Array.mapi (fun j t -> (Imbr (mind,j),t)) (Rtree.mk_rec_calls ntypes) in
+  let rc = Array.mapi (fun j t -> (Nested (NestedInd (mind,j)),t)) (Rtree.mk_rec_calls ntypes) in
   let lra_ind = Array.rev_to_list rc in
   let ra_env = List.map (fun (r,t) -> (r,Rtree.lift ntypes t)) ra_env in
   (env, lra_ind @ ra_env)
@@ -637,6 +642,11 @@ let abstract_mind_lc ntyps npars lc =
     in
     Array.map (substl make_abs) lc
 
+let is_primitive_positive_container env c =
+  match env.retroknowledge.Retroknowledge.retro_array with
+  | Some c' when Constant.equal c c' -> true
+  | _ -> false
+
 (* [get_recargs_approx env tree ind args] builds an approximation of the recargs
 tree for ind, knowing args. The argument tree is used to know when candidate
 nested types should be traversed, pruning the tree otherwise. This code is very
@@ -657,8 +667,14 @@ let get_recargs_approx env tree ind args =
        (* When the inferred tree allows it, we consider that we have a potential
        nested inductive type *)
        begin match dest_recarg tree with
-             | Imbr kn' | Mrec kn' when eq_ind (fst ind_kn) kn' ->
-                           build_recargs_nested ienv tree (ind_kn, largs)
+             | Nested (NestedInd kn') | Mrec kn' when eq_ind (fst ind_kn) kn' ->
+               build_recargs_nested ienv tree (ind_kn, largs)
+             | _ -> mk_norec
+       end
+    | Const (c,_) when is_primitive_positive_container env c ->
+       begin match dest_recarg tree with
+             | Nested (NestedPrimitive c') when Constant.equal c c' ->
+               build_recargs_nested_primitive ienv tree (c, largs)
              | _ -> mk_norec
        end
     | _err ->
@@ -696,11 +712,21 @@ let get_recargs_approx env tree ind args =
          build_recargs_constructors ienv' trees.(j).(k) c')
         auxlcvect
       in
-      mk_paths (Imbr (mind,j)) paths
+      mk_paths (Nested (NestedInd (mind,j))) paths
     in
     let irecargs = Array.mapi mk_irecargs mib.mind_packets in
     (Rtree.mk_rec irecargs).(i)
 
+  and build_recargs_nested_primitive (env, ra_env) tree (c, largs) =
+    if eq_wf_paths tree mk_norec then tree
+    else
+    let ntypes = 1 in (* Primitive types are modelled by non-mutual inductive types *)
+    let ra_env = List.map (fun (r,t) -> (r,Rtree.lift ntypes t)) ra_env in
+    let ienv = (env, ra_env) in
+    let paths = List.map2 (build_recargs ienv) (dest_subterms tree).(0) largs in
+    let recargs = [| mk_paths (Nested (NestedPrimitive c)) [| paths |] |] in
+    (Rtree.mk_rec recargs).(0)
+
   and build_recargs_constructors ienv trees c =
     let rec recargs_constr_rec (env,_ra_env as ienv) trees lrec c =
       let x,largs = decompose_app (whd_all env c) in
@@ -829,8 +855,17 @@ let rec subterm_specif renv stack t =
        | Dead_code -> Dead_code
        | Not_subterm -> Not_subterm)
 
-    | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _
-      | Construct _ | CoFix _ | Int _ | Float _ -> Not_subterm
+    | Const c ->
+      begin try
+        let _ = Environ.constant_value_in renv.env c in Not_subterm
+      with
+        | NotEvaluableConst (IsPrimitive (_u,op)) when List.length l >= CPrimitives.arity op ->
+          primitive_specif renv op l
+        | NotEvaluableConst _ -> Not_subterm
+      end
+
+    | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Ind _
+      | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> Not_subterm
 
 
       (* Other terms are not subterms *)
@@ -846,6 +881,24 @@ and extract_stack = function
    | [] -> Lazy.from_val Not_subterm , []
    | h::t -> stack_element_specif h, t
 
+and primitive_specif renv op args =
+  let open CPrimitives in
+  match op with
+  | Arrayget | Arraydefault ->
+    (* t.[i] and default t can be seend as strict subterms of t, with a
+       potentially nested rectree. *)
+    let arg = List.nth args 1 in (* the result is a strict subterm of the second argument *)
+    let subt = subterm_specif renv [] arg in
+    begin match subt with
+    | Subterm (_s, wf) ->
+      let wf_args = (dest_subterms wf).(0) in
+      spec_of_tree (List.nth wf_args 0) (* first and only parameter of `array` *)
+    | Dead_code -> Dead_code
+    | Not_subterm -> Not_subterm
+    end
+  | _ -> Not_subterm
+
+
 (* Check term c can be applied to one of the mutual fixpoints. *)
 let check_is_subterm x tree =
   match Lazy.force x with
@@ -1086,6 +1139,12 @@ let check_one_fix renv recpos trees def =
         | Sort _ | Int _ | Float _ ->
           assert (List.is_empty l)
 
+        | Array (_u, t,def,ty) ->
+          assert (List.is_empty l);
+          Array.iter (check_rec_call renv []) t;
+          check_rec_call renv [] def;
+          check_rec_call renv [] ty
+
         (* l is not checked because it is considered as the meta's context *)
         | (Evar _ | Meta _) -> ()
 
@@ -1278,7 +1337,7 @@ let check_one_cofix env nbfix def deftype =
         | Evar _ ->
             List.iter (check_rec_call env alreadygrd n tree vlra) args
         | Rel _ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _
-          | Ind _ | Fix _ | Proj _ | Int _ | Float _ ->
+          | Ind _ | Fix _ | Proj _ | Int _ | Float _ | Array _ ->
            raise (CoFixGuardError (env,NotGuardedForm t)) in
 
   let ((mind, _),_) = codomain_is_coind env deftype in
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 9f865f8f01..78658dc4de 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -105,6 +105,13 @@ val check_case_info : env -> pinductive -> Sorts.relevance -> case_info -> unit
 
 (** {6 Guard conditions for fix and cofix-points. } *)
 
+(** [is_primitive_positive_container env c] tells if the constant [c] is
+    registered as a primitive type that can be seen as a container where the
+    occurrences of its parameters are positive, in which case the positivity and
+    guard conditions are extended to allow inductive types to nest their subterms
+    in these containers. *)
+val is_primitive_positive_container : env -> Constant.t -> bool
+
 (** When [chk] is false, the guard condition is not actually
     checked. *)
 val check_fix : env -> fixpoint -> unit
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index 71a3e95d25..8191a5b0f3 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -138,6 +138,13 @@ let rec infer_fterm cv_pb infos variances hd stk =
     let le = Esubst.subs_liftn n e in
     let variances = infer_vect infos variances (Array.map (mk_clos le) cl) in
     infer_stack infos variances stk
+  | FArray (u,elemsdef,ty) ->
+    let variances = infer_generic_instance_eq variances u in
+    let variances = infer_fterm CONV infos variances ty [] in
+    let elems, def = Parray.to_array elemsdef in
+    let variances = infer_fterm CONV infos variances def [] in
+    let variances = infer_vect infos variances elems in
+    infer_stack infos variances stk
 
   | FCaseInvert (_,p,_,_,br,e) ->
     let infer c variances = infer_fterm CONV infos variances (mk_clos e c) [] in
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index cc9da3a2ce..41388d9f17 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -1,8 +1,8 @@
 Names
 TransparentState
 Uint63
+Parray
 Float64
-CPrimitives
 Univ
 UGraph
 Esubst
@@ -12,6 +12,7 @@ Context
 Constr
 Vars
 Term
+CPrimitives
 Mod_subst
 Vmvalues
 Cbytecodes
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index c8cee7db73..ae070e6f8e 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -259,6 +259,7 @@ type primitive =
   | Mk_proj
   | Is_int
   | Is_float
+  | Is_parray
   | Cast_accu
   | Upd_cofix
   | Force_cofix
@@ -285,7 +286,8 @@ type primitive =
   | MLmagic
   | MLarrayget
   | Mk_empty_instance
-  | Coq_primitive of CPrimitives.t * (prefix * pconstant) option
+  | MLparray_of_array
+  | Coq_primitive of CPrimitives.t * bool (* check for accu *)
 
 let eq_primitive p1 p2 =
   match p1, p2 with
@@ -346,15 +348,15 @@ let primitive_hash = function
   | MLsub -> 31
   | MLmul -> 32
   | MLmagic -> 33
-  | Coq_primitive (prim, None) -> combinesmall 34 (CPrimitives.hash prim)
-  | Coq_primitive (prim, Some (prefix,(kn,_))) ->
-     combinesmall 35 (combine3 (String.hash prefix) (Constant.hash kn) (CPrimitives.hash prim))
-  | Mk_proj -> 36
-  | MLarrayget -> 37
-  | Mk_empty_instance -> 38
-  | Mk_float -> 39
-  | Is_float -> 40
+  | Coq_primitive (prim, b) -> combinesmall 34 (combine (CPrimitives.hash prim) (Hashtbl.hash b))
+  | Mk_proj -> 35
+  | MLarrayget -> 36
+  | Mk_empty_instance -> 37
+  | Mk_float -> 38
+  | Is_float -> 39
+  | Is_parray -> 41
   | MLnot -> 41
+  | MLparray_of_array -> 42
 
 type mllambda =
   | MLlocal        of lname
@@ -971,11 +973,14 @@ type prim_aux =
 
 let add_check cond targs args =
   let aux cond t a =
-    match a with
-    | PAml(MLint _) -> cond
-    | PAml ml ->
+    match t, a with
+    | CPrimitives.(PITT_type (PT_int63, _)), PAml(MLapp(MLprimitive Mk_uint, _)) -> cond
+    | CPrimitives.(PITT_type (PT_array, _)), PAml(MLapp(MLprimitive MLparray_of_array, _)) -> cond
+    | CPrimitives.(PITT_type (PT_array, _)), PAml(MLapp (MLglobal (Ginternal "get_value"),_)) -> cond
+    | CPrimitives.(PITT_type (prim_ty, _)), PAml ml ->
        (* FIXME: use explicit equality function *)
-       if List.mem (t, ml) cond then cond else (t, ml)::cond
+       let c = (CPrimitives.PTE prim_ty, ml) in
+       if List.mem c cond then cond else c::cond
     | _ -> cond
   in
   Array.fold_left2 aux cond targs args
@@ -985,13 +990,15 @@ let extract_prim ml_of l =
   let cond = ref [] in
   let type_args p =
     let rec aux = function [] | [_] -> [] | h :: t -> h :: aux t in
-    Array.of_list (aux (CPrimitives.types p)) in
+    let params, sign = CPrimitives.types p in
+    List.length params, Array.of_list (aux sign) in
   let rec aux l =
     match l with
     | Lprim(prefix,kn,p,args) ->
-      let targs = type_args p in
+      let nparams, targs = type_args p in
       let args = Array.map aux args in
-      cond := add_check !cond targs args;
+      let checked_args = Array.init (Array.length args - nparams) (fun i -> args.(i+nparams)) in
+      cond := add_check !cond targs checked_args;
       PAprim(prefix,kn,p,args)
     | Lrel _ | Lvar _ | Luint _ | Lval _ | Lconst _ -> PAml (ml_of l)
     | _ ->
@@ -1006,31 +1013,48 @@ let cast_to_int v =
   | MLint _ -> v
   | _ -> MLapp(MLprimitive Val_to_int, [|v|])
 
-let compile_prim decl cond paux =
+let ml_of_instance instance u =
+  let ml_of_level l =
+    match Univ.Level.var_index l with
+    | Some i ->
+       let univ = MLapp(MLprimitive MLmagic, [|MLlocal (Option.get instance)|]) in
+       mkMLapp (MLprimitive MLarrayget) [|univ; MLint i|]
+    | None -> let i = push_symbol (SymbLevel l) in get_level_code i
+  in
+  let u = Univ.Instance.to_array u in
+  if Array.is_empty u then [||]
+  else let u = Array.map ml_of_level u in
+       [|MLapp (MLprimitive MLmagic, [|MLarray u|])|]
+
+let compile_prim env decl cond paux =
 
   let rec opt_prim_aux paux =
     match paux with
     | PAprim(_prefix, _kn, op, args) ->
-      let args = Array.map opt_prim_aux args in
-      app_prim (Coq_primitive(op,None)) args
+      let n = CPrimitives.nparams op in
+      let args = Array.map opt_prim_aux (Array.sub args n (Array.length args - n)) in
+      app_prim (Coq_primitive(op, false)) args
     | PAml ml -> ml
 
   and naive_prim_aux paux =
     match paux with
-    | PAprim(prefix, kn, op, args) ->
-      app_prim (Coq_primitive(op, Some (prefix,kn))) (Array.map naive_prim_aux args)
+    | PAprim(prefix, (kn,u), op, args) ->
+      let uarg = ml_of_instance env.env_univ u in
+      let prim_const = mkMLapp (MLglobal (Gconstant(prefix,kn))) uarg in
+      let prim = mkMLapp (MLprimitive(Coq_primitive(op, true))) [|prim_const|] in
+      mkMLapp prim (Array.map naive_prim_aux args)
     | PAml ml -> ml
   in
 
   let compile_cond cond paux =
     match cond with
     | [] -> opt_prim_aux paux
-    | [CPrimitives.(PITT_type PT_int63), c1] ->
+    | [CPrimitives.(PTE PT_int63), c1] ->
       MLif(app_prim Is_int [|c1|], opt_prim_aux paux, naive_prim_aux paux)
     | _ ->
-      let ci, cf =
+      let ci, co =
         let is_int =
-          function CPrimitives.(PITT_type PT_int63), _ -> true | _ -> false in
+          function CPrimitives.(PTE PT_int63), _ -> true | _ -> false in
         List.partition is_int cond in
       let condi =
         let cond =
@@ -1038,21 +1062,25 @@ let compile_prim decl cond paux =
             (fun ml (_, c) -> app_prim MLland [| ml; cast_to_int c|])
             (MLint 0) ci in
         app_prim MLmagic [|cond|] in
-      let condf = match cf with
+      let condo = match co with
         | [] -> MLint 0
-        | [_, c1] -> app_prim Is_float [|c1|]
-        | (_, c1) :: condf ->
+        | (CPrimitives.PTE ty, c1) :: condo ->
+          let check = match ty with
+          | CPrimitives.PT_float64 -> Is_float
+          | CPrimitives.PT_array -> Is_parray
+          | CPrimitives.PT_int63 -> assert false
+          in
            List.fold_left
-             (fun ml (_, c) -> app_prim MLand [| ml; app_prim Is_float [|c|]|])
-             (app_prim Is_float [|c1|]) condf in
-      match ci, cf with
+             (fun ml (_, c) -> app_prim MLand [| ml; app_prim check [|c|]|])
+             (app_prim check [|c1|]) condo in
+      match ci, co with
       | [], [] -> opt_prim_aux paux
       | _ :: _, [] ->
          MLif(condi, naive_prim_aux paux, opt_prim_aux paux)
       | [], _ :: _ ->
-         MLif(condf, opt_prim_aux paux, naive_prim_aux paux)
+         MLif(condo, opt_prim_aux paux, naive_prim_aux paux)
       | _ :: _, _ :: _ ->
-         let cond = app_prim MLand [|condf; app_prim MLnot [|condi|]|] in
+         let cond = app_prim MLand [|condo; app_prim MLnot [|condi|]|] in
          MLif(cond, opt_prim_aux paux, naive_prim_aux paux) in
 
   let add_decl decl body =
@@ -1065,19 +1093,6 @@ let compile_prim decl cond paux =
   else
     add_decl decl (compile_cond cond paux)
 
-let ml_of_instance instance u =
-  let ml_of_level l =
-    match Univ.Level.var_index l with
-    | Some i ->
-       let univ = MLapp(MLprimitive MLmagic, [|MLlocal (Option.get instance)|]) in
-       mkMLapp (MLprimitive MLarrayget) [|univ; MLint i|]
-    | None -> let i = push_symbol (SymbLevel l) in get_level_code i
-  in
-  let u = Univ.Instance.to_array u in
-  if Array.is_empty u then [||]
-  else let u = Array.map ml_of_level u in
-       [|MLapp (MLprimitive MLmagic, [|MLarray u|])|]
-
  let rec ml_of_lam env l t =
   match t with
   | Lrel(id ,i) -> get_rel env id i
@@ -1118,7 +1133,7 @@ let ml_of_instance instance u =
   | Lproj (prefix, ind, i) -> MLglobal(Gproj (prefix, ind, i))
   | Lprim _ ->
     let decl,cond,paux = extract_prim (ml_of_lam env l) t in
-    compile_prim decl cond paux
+    compile_prim env decl cond paux
   | Lcase (annot,p,a,bs) ->
       (* let predicate_uid fv_pred = compilation of p
          let rec case_uid fv a_uid =
@@ -1333,6 +1348,9 @@ let ml_of_instance instance u =
      MLconstruct(prefix,cn,tag,args)
   | Luint i -> MLapp(MLprimitive Mk_uint, [|MLuint i|])
   | Lfloat f -> MLapp(MLprimitive Mk_float, [|MLfloat f|])
+  | Lparray (t,def) ->
+    let def = ml_of_lam env l def in
+    MLapp(MLprimitive MLparray_of_array, [| MLarray (Array.map (ml_of_lam env l) t); def |])
   | Lval v ->
       let i = push_symbol (SymbValue v) in get_value_code i
   | Lsort s ->
@@ -1777,6 +1795,7 @@ let pp_mllam fmt l =
     | Mk_proj -> Format.fprintf fmt "mk_proj_accu"
     | Is_int -> Format.fprintf fmt "is_int"
     | Is_float -> Format.fprintf fmt "is_float"
+    | Is_parray -> Format.fprintf fmt "is_parray"
     | Cast_accu -> Format.fprintf fmt "cast_accu"
     | Upd_cofix -> Format.fprintf fmt "upd_cofix"
     | Force_cofix -> Format.fprintf fmt "force_cofix"
@@ -1803,11 +1822,10 @@ let pp_mllam fmt l =
     | MLmagic -> Format.fprintf fmt "Obj.magic"
     | MLarrayget -> Format.fprintf fmt "Array.get"
     | Mk_empty_instance -> Format.fprintf fmt "Univ.Instance.empty"
-    | Coq_primitive (op,None) ->
+    | MLparray_of_array -> Format.fprintf fmt "parray_of_array"
+    | Coq_primitive (op, false) ->
        Format.fprintf fmt "no_check_%s" (CPrimitives.to_string op)
-    | Coq_primitive (op, Some (prefix,(c,_))) ->
-        Format.fprintf fmt "%s %a" (CPrimitives.to_string op)
-                       pp_mllam (MLglobal (Gconstant (prefix,c)))
+    | Coq_primitive (op, true) -> Format.fprintf fmt "%s" (CPrimitives.to_string op)
   in
   Format.fprintf fmt "@[%a@]" pp_mllam l
 
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 31a716a786..01e9550ec5 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -38,6 +38,10 @@ let rec conv_val env pb lvl v1 v2 cu =
     | Vfloat64 f1, Vfloat64 f2 ->
         if Float64.(equal (of_float f1) (of_float f2)) then cu
         else raise NotConvertible
+    | Varray t1, Varray t2 ->
+      let len = Parray.length_int t1 in
+      if not (Int.equal len (Parray.length_int t2)) then raise NotConvertible;
+      Parray.fold_left2 (fun cu v1 v2 -> conv_val env CONV lvl v1 v2 cu) cu t1 t2
     | Vblock b1, Vblock b2 ->
         let n1 = block_size b1 in
         let n2 = block_size b2 in
@@ -51,7 +55,7 @@ let rec conv_val env pb lvl v1 v2 cu =
             aux lvl max b1 b2 (i+1) cu
         in
         aux lvl (n1-1) b1 b2 0 cu
-    | (Vaccu _ | Vconst _ | Vint64 _ | Vfloat64 _ | Vblock _), _ -> raise NotConvertible
+    | (Vaccu _ | Vconst _ | Vint64 _ | Vfloat64 _ | Varray _ | Vblock _), _ -> raise NotConvertible
 
 and conv_accu env pb lvl k1 k2 cu =
   let n1 = accu_nargs k1 in
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 3819cfd8ee..b00b96018f 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -40,6 +40,7 @@ type lambda =
   | Lfix          of (int array * (string * inductive) array * int) * fix_decl
   | Lcofix        of int * fix_decl
   | Lint          of int (* a constant constructor *)
+  | Lparray       of lambda array * lambda
   | Lmakeblock    of prefix * inductive * int * lambda array
                   (* prefix, inductive name, constructor tag, arguments *)
         (* A fully applied non-constant constructor *)
@@ -187,6 +188,10 @@ let map_lam_with_binders g f n lam =
   | Levar (evk, args) ->
     let args' = Array.Smart.map (f n) args in
     if args == args' then lam else Levar (evk, args')
+  | Lparray (p,def) ->
+      let p' = Array.Smart.map (f n) p in
+      let def' = f n def in
+      if def' == def && p == p' then lam else Lparray (p', def')
 
 (*s Lift and substitution *)
 
@@ -377,6 +382,12 @@ let makeblock env ind tag nparams arity args =
     let prefix = get_mind_prefix env (fst ind) in
     Lmakeblock(prefix, ind, tag, args)
 
+let makearray args def =
+  try
+    let p = Array.map get_value args in
+    Lval (Nativevalues.parray_of_array p (get_value def))
+  with Not_found -> Lparray (args, def)
+
 (* Translation of constants *)
 
 let rec get_alias env (kn, u as p) =
@@ -400,8 +411,13 @@ let expand_prim env kn op arity =
 
 let lambda_of_prim env kn op args =
   let arity = CPrimitives.arity op in
-  if Array.length args >= arity then prim env kn op args
-  else mkLapp (expand_prim env kn op arity) args
+  match Int.compare (Array.length args) arity with
+  | 0 -> prim env kn op args
+  | x when x > 0 ->
+    let prim_args = Array.sub args 0 arity in
+    let extra_args = Array.sub args arity (Array.length args - arity) in
+    mkLapp(prim env kn op prim_args) extra_args
+  | _ -> mkLapp (expand_prim env kn op arity) args
 
 (*i Global environment *)
 
@@ -589,6 +605,10 @@ let rec lambda_of_constr cache env sigma c =
 
   | Float f -> Lfloat f
 
+  | Array (_u, t, def, _ty) ->
+    let def = lambda_of_constr cache env sigma def in
+    makearray (lambda_of_args cache env sigma 0 t) def
+
 and lambda_of_app cache env sigma f args =
   match kind f with
   | Const (_kn,_u as c) ->
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index e339286329..619d362f35 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -34,6 +34,7 @@ type lambda =
   | Lfix          of (int array * (string * inductive) array * int) * fix_decl
   | Lcofix        of int * fix_decl
   | Lint          of int (* a constant constructor *)
+  | Lparray       of lambda array * lambda
   | Lmakeblock    of prefix * inductive * int * lambda array
                   (* prefix, inductive name, constructor tag, arguments *)
         (* A fully applied non-constant constructor *)
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index a5fcfae1fc..9e17f97a56 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -244,6 +244,7 @@ type kind_of_value =
   | Vconst of int
   | Vint64 of int64
   | Vfloat64 of float
+  | Varray of t Parray.t
   | Vblock of block
 
 let kind_of_value (v:t) =
@@ -253,7 +254,8 @@ let kind_of_value (v:t) =
   else
     let tag = Obj.tag o in
     if Int.equal tag accumulate_tag then
-      Vaccu (Obj.magic v)
+      if Int.equal (Obj.size o) 1 then Varray (Obj.magic v)
+      else Vaccu (Obj.magic v)
     else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v)
     else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v)
     else if (tag < Obj.lazy_tag) then Vblock (Obj.magic v)
@@ -686,6 +688,84 @@ let next_down accu x =
   if is_float x then no_check_next_down x
   else accu x
 
+let is_parray t =
+  let t = Obj.magic t in
+  Obj.is_block t && Obj.size t = 1
+
+let to_parray t = Obj.magic t
+let of_parray t = Obj.magic t
+
+let no_check_arraymake n def =
+  of_parray (Parray.make (to_uint n) def)
+
+let arraymake accu vA n def =
+  if is_int n then
+    no_check_arraymake n def
+  else accu vA n def
+
+let no_check_arrayget t n =
+   Parray.get (to_parray t) (to_uint n)
+[@@ocaml.inline always]
+
+let arrayget accu vA t n =
+  if is_parray t && is_int n then
+    no_check_arrayget t n
+  else accu vA t n
+
+let no_check_arraydefault t =
+  Parray.default (to_parray t)
+[@@ocaml.inline always]
+
+let arraydefault accu vA t =
+  if is_parray t then
+    no_check_arraydefault t
+  else accu vA t
+
+let no_check_arrayset t n v =
+  of_parray (Parray.set (to_parray t) (to_uint n) v)
+[@@ocaml.inline always]
+
+let arrayset accu vA t n v =
+  if is_parray t && is_int n then
+    no_check_arrayset t n v
+  else accu vA t n v
+
+let no_check_arraycopy t =
+  of_parray (Parray.copy (to_parray t))
+[@@ocaml.inline always]
+
+let arraycopy accu vA t =
+  if is_parray t then
+    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]
+
+let arraylength accu vA t =
+  if is_parray t then
+    no_check_arraylength t
+  else accu vA t
+
+let parray_of_array t def =
+  (Obj.magic (Parray.unsafe_of_array t def) : t)
+
+let arrayinit n (f:t->t) def =
+  of_parray (Parray.init (to_uint n) (Obj.magic f) def)
+
+let arraymap f t =
+  of_parray (Parray.map f (to_parray t))
+
 let hobcnv = Array.init 256 (fun i -> Printf.sprintf "%02x" i)
 let bohcnv = Array.init 256 (fun i -> i -
                                       (if 0x30 <= i then 0x30 else 0) -
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 78a9b2ea13..08c5bd7126 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -134,6 +134,7 @@ type kind_of_value =
   | Vconst of int
   | Vint64 of int64
   | Vfloat64 of float
+  | Varray of t Parray.t
   | Vblock of block
 
 val kind_of_value : t -> kind_of_value
@@ -332,3 +333,39 @@ val no_check_next_up : t -> t
 
 val no_check_next_down : t -> t
 [@@ocaml.inline always]
+
+(** Support for arrays *)
+
+val parray_of_array : t array -> t -> t
+val is_parray : t -> bool
+
+val arraymake : t -> t -> t -> t -> t (* accu A n def *)
+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 *)
+
+val no_check_arraymake : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_arrayget : t -> t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_arraydefault : t -> t
+[@@ocaml.inline always]
+
+val no_check_arrayset : t -> t -> t -> t
+[@@ocaml.inline always]
+
+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.ml b/kernel/parray.ml
new file mode 100644
index 0000000000..ea314c1883
--- /dev/null
+++ b/kernel/parray.ml
@@ -0,0 +1,124 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+let max_array_length32 = 4194303
+
+let max_length = Uint63.of_int max_array_length32
+
+let length_to_int i = snd (Uint63.to_int2 i)
+
+let trunc_size n =
+  if Uint63.le Uint63.zero n && Uint63.lt n (Uint63.of_int max_array_length32) then
+    length_to_int n
+  else max_array_length32
+
+type 'a t = ('a kind) ref
+and 'a kind =
+  | Array of 'a array * 'a
+  | Updated of int * 'a * 'a t
+
+let unsafe_of_array t def = ref (Array (t,def))
+let of_array t def = unsafe_of_array (Array.copy t) def
+
+let rec length_int p =
+  match !p with
+  | Array (t,_) -> Array.length t
+  | Updated (_, _, p) -> length_int p
+
+let length p = Uint63.of_int @@ length_int p
+
+let rec get p n =
+  match !p with
+  | Array (t,def) ->
+      let l = Array.length t in
+      if Uint63.le Uint63.zero n && Uint63.lt n (Uint63.of_int l) then
+        Array.unsafe_get t (length_to_int n)
+      else def
+  | Updated (k,e,p) ->
+     if Uint63.equal n (Uint63.of_int k) then e
+     else get p n
+
+let set p n e =
+  let kind = !p in
+  match kind with
+  | Array (t,_) ->
+      let l = Uint63.of_int @@ Array.length t in
+      if Uint63.le Uint63.zero n && Uint63.lt n l then
+        let res = ref kind in
+        let n = length_to_int n in
+        p := Updated (n, Array.unsafe_get t n, res);
+        Array.unsafe_set t n e;
+        res
+      else p
+  | Updated _ ->
+      if Uint63.le Uint63.zero n && Uint63.lt n (length p) then
+        ref (Updated((length_to_int n), e, p))
+      else p
+
+let rec default p =
+  match !p with
+  | Array (_,def) -> def
+  | Updated (_,_,p) -> default p
+
+let make n def =
+  ref (Array (Array.make (trunc_size n) def, def))
+
+let init n f def =
+  let n = trunc_size n in
+  let t = Array.init n f in
+  ref (Array (t, def))
+
+let rec to_array p =
+  match !p with
+  | Array (t,def) -> Array.copy t, def
+  | Updated (n,e,p) ->
+      let (t,_) as r = to_array p in
+      Array.unsafe_set t n e; r
+
+let copy p =
+  let (t,def) = to_array p in
+  ref (Array (t,def))
+
+let rec rerootk t k =
+  match !t with
+  | Array _ -> k ()
+  | Updated (i, v, t') ->
+      let k' () =
+        begin match !t' with
+        | Array (a,_def) as n ->
+            let v' = a.(i) in
+            Array.unsafe_set a i v;
+            t := n;
+            t' := Updated (i, v', t)
+        | Updated _ -> assert false
+        end; k() in
+      rerootk t' k'
+
+let reroot t = rerootk t (fun () -> t)
+
+let map f p =
+  let p = reroot p in
+  match !p with
+  | Array (t,def) -> ref (Array (Array.map f t, f def))
+  | Updated _ -> assert false
+
+let fold_left f x p =
+  let p = reroot p in
+  match !p with
+  | Array (t,def) -> f (Array.fold_left f x t) def
+  | Updated _ -> assert false
+
+let fold_left2 f a p1 p2 =
+  let p1 = reroot p1 in
+  let p2 = reroot p2 in
+  match !p1, !p2 with
+  | Array (t1, def1), Array (t2, def2) ->
+    f (CArray.fold_left2 f a t1 t2) def1 def2
+  | _ -> assert false
diff --git a/kernel/parray.mli b/kernel/parray.mli
new file mode 100644
index 0000000000..0276278bd0
--- /dev/null
+++ b/kernel/parray.mli
@@ -0,0 +1,36 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+val max_length : Uint63.t
+
+type 'a t
+val length  : 'a t -> Uint63.t
+val length_int : 'a t -> int
+val get     : 'a t -> Uint63.t -> 'a
+val set     : 'a t -> Uint63.t -> 'a -> 'a t
+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
+
+val to_array : 'a t -> 'a array * 'a (* default *)
+
+val of_array : 'a array -> 'a (* default *) -> 'a t
+
+val unsafe_of_array : 'a array -> 'a -> 'a t
+(* [unsafe_of_array] injects a mutable array into a persistent one, but does
+   not perform a copy. This means that if the persistent array is mutated, the
+   original one will be too. *)
+
+val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a
+val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b t -> 'c t -> 'a
diff --git a/kernel/primred.ml b/kernel/primred.ml
index c475828cb3..10a8da8813 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -21,6 +21,13 @@ let add_retroknowledge env action =
       | None -> { retro with retro_float64 = Some c }
       | Some c' -> assert (Constant.equal c c'); retro in
     set_retroknowledge env retro
+  | Register_type(PT_array,c) ->
+    let retro = env.retroknowledge in
+    let retro =
+      match retro.retro_array with
+      | None -> { retro with retro_array = Some c }
+      | Some c' -> assert (Constant.equal c c'); retro in
+    set_retroknowledge env retro
   | Register_ind(pit,ind) ->
     let retro = env.retroknowledge in
     let retro =
@@ -120,10 +127,12 @@ module type RedNativeEntries =
     type elem
     type args
     type evd (* will be unit in kernel, evar_map outside *)
+    type uinstance
 
     val get : args -> int -> elem
     val get_int : evd -> elem -> Uint63.t
     val get_float : evd -> elem -> Float64.t
+    val get_parray : evd -> elem -> elem Parray.t
     val mkInt : env -> Uint63.t -> elem
     val mkFloat : env -> Float64.t -> elem
     val mkBool : env -> bool -> elem
@@ -146,6 +155,7 @@ module type RedNativeEntries =
     val mkPInf : env -> elem
     val mkNInf : env -> elem
     val mkNaN : env -> elem
+    val mkArray : env -> uinstance -> elem Parray.t -> elem -> elem
   end
 
 module type RedNative =
@@ -153,17 +163,20 @@ module type RedNative =
    type elem
    type args
    type evd
-   val red_prim : env -> evd -> CPrimitives.t -> args -> elem option
+   type uinstance
+   val red_prim : env -> evd -> CPrimitives.t -> uinstance -> args -> elem option
  end
 
 module RedNative (E:RedNativeEntries) :
   RedNative with type elem = E.elem
   with type args = E.args
-  with type evd = E.evd =
+  with type evd = E.evd
+  with type uinstance = E.uinstance =
 struct
   type elem = E.elem
   type args = E.args
   type evd = E.evd
+  type uinstance = E.uinstance
 
   let get_int evd args i = E.get_int evd (E.get args i)
 
@@ -180,7 +193,9 @@ struct
 
   let get_float2 evd args = get_float evd args 0, get_float evd args 1
 
-  let red_prim_aux env evd op args =
+  let get_parray evd args i = E.get_parray evd (E.get args i)
+
+  let red_prim_aux env evd op u args =
     let open CPrimitives in
     match op with
     | Int63head0 ->
@@ -315,11 +330,43 @@ struct
       let f = get_float1 evd args in E.mkFloat env (Float64.next_up f)
     | Float64next_down ->
       let f = get_float1 evd args in E.mkFloat env (Float64.next_down f)
+    | Arraymake ->
+      let ty = E.get args 0 in
+      let i = get_int evd args 1 in
+      let d = E.get args 2 in
+      E.mkArray env u (Parray.make i d) ty
+    | Arrayget ->
+      let t = get_parray evd args 1 in
+      let i = get_int evd args 2 in
+      Parray.get t i
+    | Arraydefault ->
+      let t = get_parray evd args 1 in
+      Parray.default t
+    | Arrayset ->
+      let ty = E.get args 0 in
+      let t = get_parray evd args 1 in
+      let i = get_int evd args 2 in
+      let a = E.get args 3 in
+      let t' = Parray.set t i a in
+      E.mkArray env u t' ty
+    | Arraycopy ->
+      let ty = E.get args 0 in
+      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)
 
-  let red_prim env evd p args =
+  let red_prim env evd p u args =
     try
       let r =
-        red_prim_aux env evd p args
+        red_prim_aux env evd p u args
       in Some r
     with NativeDestKO -> None
 
diff --git a/kernel/primred.mli b/kernel/primred.mli
index bbe564d8e7..1bfaffaa44 100644
--- a/kernel/primred.mli
+++ b/kernel/primred.mli
@@ -24,10 +24,12 @@ module type RedNativeEntries =
     type elem
     type args
     type evd (* will be unit in kernel, evar_map outside *)
+    type uinstance
 
     val get : args -> int -> elem
     val get_int : evd -> elem -> Uint63.t
     val get_float : evd -> elem -> Float64.t
+    val get_parray : evd -> elem -> elem Parray.t
     val mkInt : env -> Uint63.t -> elem
     val mkFloat : env -> Float64.t -> elem
     val mkBool : env -> bool -> elem
@@ -50,6 +52,7 @@ module type RedNativeEntries =
     val mkPInf : env -> elem
     val mkNInf : env -> elem
     val mkNaN : env -> elem
+    val mkArray : env -> uinstance -> elem Parray.t -> elem -> elem
   end
 
 module type RedNative =
@@ -57,7 +60,8 @@ module type RedNative =
    type elem
    type args
    type evd
-   val red_prim : env -> evd -> CPrimitives.t -> args -> elem option
+   type uinstance
+   val red_prim : env -> evd -> CPrimitives.t -> uinstance -> args -> elem option
  end
 
 module RedNative :
@@ -65,3 +69,4 @@ module RedNative :
     RedNative with type elem = E.elem
     with type args = E.args
     with type evd = E.evd
+    with type uinstance = E.uinstance
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index e4b0bb17d4..0754e9d4cc 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -138,10 +138,10 @@ let nf_betaiota env t =
 let whd_betaiotazeta env x =
   match kind x with
   | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
-       Prod _|Lambda _|Fix _|CoFix _|Int _|Float _) -> x
+       Prod _|Lambda _|Fix _|CoFix _|Int _|Float _|Array _) -> x
     | App (c, _) ->
       begin match kind c with
-      | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | Int _ | Float _ -> x
+      | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | Int _ | Float _ | Array _ -> x
       | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
         | Case _ | Fix _ | CoFix _ | Proj _ ->
          whd_val (create_clos_infos betaiotazeta env) (create_tab ()) (inject x)
@@ -152,10 +152,10 @@ let whd_betaiotazeta env x =
 let whd_all env t =
   match kind t with
     | (Sort _|Meta _|Evar _|Ind _|Construct _|
-       Prod _|Lambda _|Fix _|CoFix _|Int _|Float _) -> t
+       Prod _|Lambda _|Fix _|CoFix _|Int _|Float _|Array _) -> t
     | App (c, _) ->
       begin match kind c with
-      | Ind _ | Construct _ | Evar _ | Meta _ | Int _ | Float _ -> t
+      | Ind _ | Construct _ | Evar _ | Meta _ | Int _ | Float _ | Array _ -> t
       | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
         | Const _ |Case _ | Fix _ | CoFix _ | Proj _ ->
          whd_val (create_clos_infos all env) (create_tab ()) (inject t)
@@ -166,10 +166,10 @@ let whd_all env t =
 let whd_allnolet env t =
   match kind t with
     | (Sort _|Meta _|Evar _|Ind _|Construct _|
-       Prod _|Lambda _|Fix _|CoFix _|LetIn _|Int _|Float _) -> t
+       Prod _|Lambda _|Fix _|CoFix _|LetIn _|Int _|Float _|Array _) -> t
     | App (c, _) ->
       begin match kind c with
-      | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ | Int _ | Float _ -> t
+      | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ | Int _ | Float _ | Array _ -> t
       | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | App _
         | Const _ | Case _ | Fix _ | CoFix _ | Proj _ ->
          whd_val (create_clos_infos allnolet env) (create_tab ()) (inject t)
@@ -644,13 +644,23 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
       Array.fold_right2 (fun b1 b2 cuniv -> ccnv (mk_clos e1 b1) (mk_clos e2 b2) cuniv)
         br1 br2 cuniv
 
+    | FArray (u1,t1,ty1), FArray (u2,t2,ty2) ->
+      let len = Parray.length_int t1 in
+      if not (Int.equal len (Parray.length_int t2)) then raise NotConvertible;
+      let cuniv = convert_instances ~flex:false u1 u2 cuniv in
+      let el1 = el_stack lft1 v1 in
+      let el2 = el_stack lft2 v2 in
+      let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in
+      let cuniv = Parray.fold_left2 (fun u v1 v2 -> ccnv CONV l2r infos el1 el2 v1 v2 u) cuniv t1 t2 in
+      convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+
      (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
      | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
        | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
        | (FLOCKED,_) | (_,FLOCKED) ) -> assert false
 
      | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _ | FCaseInvert _
-        | FProd _ | FEvar _ | FInt _ | FFloat _), _ -> raise NotConvertible
+        | FProd _ | FEvar _ | FInt _ | FFloat _ | FArray _), _ -> raise NotConvertible
 
 and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
   let f (l1, t1) (l2, t2) cuniv = ccnv CONV l2r infos l1 l2 t1 t2 cuniv in
diff --git a/kernel/relevanceops.ml b/kernel/relevanceops.ml
index 3dd965aca4..f12b8cba37 100644
--- a/kernel/relevanceops.ml
+++ b/kernel/relevanceops.ml
@@ -54,7 +54,7 @@ let rec relevance_of_fterm env extra lft f =
       | FRel n -> Range.get extra (Esubst.reloc_rel n lft - 1)
       | FAtom c -> relevance_of_term_extra env extra lft (Esubst.subs_id 0) c
       | FFlex key -> relevance_of_flex env key
-      | FInt _ | FFloat _ -> Sorts.Relevant
+      | FInt _ | FFloat _ | FArray _ -> Sorts.Relevant
       | FInd _ | FProd _ -> Sorts.Relevant (* types are always relevant *)
       | FConstruct (c,_) -> relevance_of_constructor env c
       | FApp (f, _) -> relevance_of_fterm env extra lft f
@@ -102,6 +102,7 @@ and relevance_of_term_extra env extra lft subs c =
   | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance
   | Proj (p, _) -> relevance_of_projection env p
   | Int _ | Float _ -> Sorts.Relevant
+  | Array _ -> Sorts.Relevant
 
   | Meta _ | Evar _ -> Sorts.Relevant (* let's assume metas and evars are relevant for now *)
 
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 4e642ca11d..f7c4b62d1f 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -19,6 +19,7 @@ open Names
 type retroknowledge = {
     retro_int63 : Constant.t option;
     retro_float64 : Constant.t option;
+    retro_array : Constant.t option;
     retro_bool : (constructor * constructor) option; (* true, false *)
     retro_carry : (constructor * constructor) option; (* C0, C1 *)
     retro_pair : constructor option;
@@ -40,6 +41,7 @@ type retroknowledge = {
 let empty = {
     retro_int63 = None;
     retro_float64 = None;
+    retro_array = None;
     retro_bool = None;
     retro_carry = None;
     retro_pair = None;
@@ -51,4 +53,4 @@ let empty = {
 
 type action =
   | Register_ind : 'a CPrimitives.prim_ind * inductive -> action
-  | Register_type : CPrimitives.prim_type * Constant.t -> action
+  | Register_type : 'a CPrimitives.prim_type * Constant.t -> action
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index bf8ec8badb..fd412cdd0a 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -13,6 +13,7 @@ open Names
 type retroknowledge = {
     retro_int63 : Constant.t option;
     retro_float64 : Constant.t option;
+    retro_array : Constant.t option;
     retro_bool : (constructor * constructor) option; (* true, false *)
     retro_carry : (constructor * constructor) option; (* C0, C1 *)
     retro_pair : constructor option;
@@ -35,4 +36,4 @@ val empty : retroknowledge
 
 type action =
   | Register_ind : 'a CPrimitives.prim_ind * inductive -> action
-  | Register_type : CPrimitives.prim_type * Constant.t -> action
+  | Register_type : 'a CPrimitives.prim_type * Constant.t -> action
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index c8c2301171..04e7a81697 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -21,13 +21,14 @@ open Constr
 open Declarations
 open Environ
 open Entries
+open Univ
 
 module NamedDecl = Context.Named.Declaration
 
 (* Insertion of constants and parameters in environment. *)
 
 type 'a effect_handler =
-  env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int)
+  env -> Constr.t -> 'a -> (Constr.t * ContextSet.t * int)
 
 let skip_trusted_seff sl b e =
   let rec aux sl b e acc =
@@ -62,55 +63,91 @@ let feedback_completion_typecheck =
 
 type typing_context =
 | MonoTyCtx of Environ.env * unsafe_type_judgment * Id.Set.t * Stateid.t option
-| PolyTyCtx of Environ.env * unsafe_type_judgment * Univ.universe_level_subst * Univ.AUContext.t * Id.Set.t * Stateid.t option
+| PolyTyCtx of Environ.env * unsafe_type_judgment * universe_level_subst * AUContext.t * Id.Set.t * Stateid.t option
 
-let infer_declaration env (dcl : constant_entry) =
-  match dcl with
-    | ParameterEntry (ctx,(t,uctx),nl) ->
-      let env = match uctx with
-        | Monomorphic_entry uctx -> push_context_set ~strict:true uctx env
-        | Polymorphic_entry (_, uctx) -> push_context ~strict:false uctx env
+let check_primitive_type env op_t u t =
+  let inft = Typeops.type_of_prim_or_type env u op_t in
+  try Reduction.default_conv ~l2r:false Reduction.CONV env inft t
+  with Reduction.NotConvertible ->
+    Type_errors.error_incorrect_primitive env (make_judge op_t inft) t
+
+let merge_unames =
+  Array.map2 (fun base user -> match user with Anonymous -> base | Name _ -> user)
+
+let infer_primitive env { prim_entry_type = utyp; prim_entry_content = p; } =
+  let open CPrimitives in
+  let auctx = CPrimitives.op_or_type_univs p in
+  let univs, typ =
+    match utyp with
+    | None ->
+      let u = UContext.instance (AUContext.repr auctx) in
+      let typ = Typeops.type_of_prim_or_type env u p in
+      let univs = if AUContext.is_empty auctx then Monomorphic ContextSet.empty
+        else Polymorphic auctx
       in
-      let j = Typeops.infer env t in
-      let usubst, univs = Declareops.abstract_universes uctx in
-      let r = Typeops.assumption_of_judgment env j in
-      let t = Vars.subst_univs_level_constr usubst j.uj_val in
-      {
-        Cooking.cook_body = Undef nl;
-        cook_type = t;
-        cook_universes = univs;
-        cook_relevance = r;
-        cook_inline = false;
-        cook_context = ctx;
-      }
+      univs, typ
 
-    (** Primitives cannot be universe polymorphic *)
-    | PrimitiveEntry ({ prim_entry_type = otyp;
-                        prim_entry_univs = uctxt;
-                        prim_entry_content = op_t;
-                      }) ->
-      let env = push_context_set ~strict:true uctxt env in
-      let ty = match otyp with
-      | Some typ ->
+    | Some (typ,Monomorphic_entry uctx) ->
+      assert (AUContext.is_empty auctx);
+      let env = push_context_set ~strict:true uctx env in
+      let u = Instance.empty in
+      let typ =
         let typ = Typeops.infer_type env typ in
-        Typeops.check_primitive_type env op_t typ.utj_val;
+        check_primitive_type env p u typ.utj_val;
         typ.utj_val
-      | None ->
-        match op_t with
-        | CPrimitives.OT_op op -> Typeops.type_of_prim env op
-        | CPrimitives.OT_type _ -> mkSet
       in
-      let cd =
-        match op_t with
-        | CPrimitives.OT_op op -> Declarations.Primitive op
-        | CPrimitives.OT_type _ -> Undef None in
-      { Cooking.cook_body = cd;
-        cook_type = ty;
-        cook_universes = Monomorphic uctxt;
-        cook_inline = false;
-        cook_context = None;
-        cook_relevance = Sorts.Relevant;
-      }
+      Monomorphic uctx, typ
+
+    | Some (typ,Polymorphic_entry (unames,uctx)) ->
+      assert (not (AUContext.is_empty auctx));
+      (* push_context will check that the universes aren't repeated in the instance
+         so comparing the sizes works *)
+      assert (AUContext.size auctx = UContext.size uctx);
+      (* No polymorphic primitive uses constraints currently *)
+      assert (Constraint.is_empty (UContext.constraints uctx));
+      let env = push_context ~strict:false uctx env in
+      (* Now we know that uctx matches the auctx *)
+      let typ = (Typeops.infer_type env typ).utj_val in
+      let () = check_primitive_type env p (UContext.instance uctx) typ in
+      let unames = merge_unames (AUContext.names auctx) unames in
+      let u, auctx = abstract_universes unames uctx in
+      let typ = Vars.subst_univs_level_constr (make_instance_subst u) typ in
+      Polymorphic auctx, typ
+  in
+  let body = match p with
+    | OT_op op -> Declarations.Primitive op
+    | OT_type _ -> Undef None
+    | OT_const c -> Def (Mod_subst.from_val (CPrimitives.body_of_prim_const c))
+  in
+  { Cooking.cook_body = body;
+    cook_type = typ;
+    cook_universes = univs;
+    cook_inline = false;
+    cook_context = None;
+    cook_relevance = Sorts.Relevant;
+  }
+
+let infer_declaration env (dcl : constant_entry) =
+  match dcl with
+  | ParameterEntry (ctx,(t,uctx),nl) ->
+    let env = match uctx with
+      | Monomorphic_entry uctx -> push_context_set ~strict:true uctx env
+      | Polymorphic_entry (_, uctx) -> push_context ~strict:false uctx env
+    in
+    let j = Typeops.infer env t in
+    let usubst, univs = Declareops.abstract_universes uctx in
+    let r = Typeops.assumption_of_judgment env j in
+    let t = Vars.subst_univs_level_constr usubst j.uj_val in
+    {
+      Cooking.cook_body = Undef nl;
+      cook_type = t;
+      cook_universes = univs;
+      cook_relevance = r;
+      cook_inline = false;
+      cook_context = ctx;
+    }
+
+  | PrimitiveEntry entry -> infer_primitive env entry
 
   | DefinitionEntry c ->
       let { const_entry_type = typ; _ } = c in
@@ -118,13 +155,13 @@ let infer_declaration env (dcl : constant_entry) =
       let env, usubst, univs = match c.const_entry_universes with
       | Monomorphic_entry ctx ->
         let env = push_context_set ~strict:true ctx env in
-        env, Univ.empty_level_subst, Monomorphic ctx
+        env, empty_level_subst, Monomorphic ctx
       | Polymorphic_entry (nas, uctx) ->
         (** [ctx] must contain local universes, such that it has no impact
             on the rest of the graph (up to transitivity). *)
         let env = push_context ~strict:false uctx env in
-        let sbst, auctx = Univ.abstract_universes nas uctx in
-        let sbst = Univ.make_instance_subst sbst in
+        let sbst, auctx = abstract_universes nas uctx in
+        let sbst = make_instance_subst sbst in
         env, sbst, Polymorphic auctx
       in
       let j = Typeops.infer env body in
@@ -171,8 +208,8 @@ let infer_opaque env = function
       let { opaque_entry_feedback = feedback_id; _ } = c in
       let env = push_context ~strict:false uctx env in
       let tj = Typeops.infer_type env typ in
-      let sbst, auctx = Univ.abstract_universes nas uctx in
-      let usubst = Univ.make_instance_subst sbst in
+      let sbst, auctx = abstract_universes nas uctx in
+      let usubst = make_instance_subst sbst in
       let context = PolyTyCtx (env, tj, usubst, auctx, c.opaque_entry_secctx, feedback_id) in
       let def = OpaqueDef () in
       let typ = Vars.subst_univs_level_constr usubst tj.utj_val in
@@ -260,7 +297,7 @@ let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_out
 | MonoTyCtx (env, tyj, declared, feedback_id) ->
   let ((body, uctx), side_eff) = body in
   let (body, uctx', valid_signatures) = handle env body side_eff in
-  let uctx = Univ.ContextSet.union uctx uctx' in
+  let uctx = ContextSet.union uctx uctx' in
   let env = push_context_set uctx env in
   let body,env,ectx = skip_trusted_seff valid_signatures body env in
   let j = Typeops.infer env body in
@@ -273,17 +310,17 @@ let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_out
 | PolyTyCtx (env, tj, usubst, auctx, declared, feedback_id) ->
   let ((body, ctx), side_eff) = body in
   let body, ctx', _ = handle env body side_eff in
-  let ctx = Univ.ContextSet.union ctx ctx' in
+  let ctx = ContextSet.union ctx ctx' in
   (** [ctx] must contain local universes, such that it has no impact
       on the rest of the graph (up to transitivity). *)
   let env = push_subgraph ctx env in
-  let private_univs = on_snd (Univ.subst_univs_level_constraints usubst) ctx in
+  let private_univs = on_snd (subst_univs_level_constraints usubst) ctx in
   let j = Typeops.infer env body in
   let _ = Typeops.judge_of_cast env j DEFAULTcast tj in
   let () = check_section_variables env declared tj.utj_val body in
   let def = Vars.subst_univs_level_constr usubst j.uj_val in
   let () = feedback_completion_typecheck feedback_id in
-  def, Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, private_univs)
+  def, Opaqueproof.PrivatePolymorphic (AUContext.size auctx, private_univs)
 
 (*s Global and local constant declaration. *)
 
@@ -325,13 +362,13 @@ let translate_local_def env _id centry =
     const_entry_secctx = centry.secdef_secctx;
     const_entry_feedback = centry.secdef_feedback;
     const_entry_type = centry.secdef_type;
-    const_entry_universes = Monomorphic_entry Univ.ContextSet.empty;
+    const_entry_universes = Monomorphic_entry ContextSet.empty;
     const_entry_inline_code = false;
   } in
   let decl = infer_declaration env (DefinitionEntry centry) in
   let typ = decl.cook_type in
   let () = match decl.cook_universes with
-  | Monomorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
+  | Monomorphic ctx -> assert (ContextSet.is_empty ctx)
   | Polymorphic _ -> assert false
   in
   let c = match decl.cook_body with
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 58a099f7f6..f86c12e1f1 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -213,9 +213,20 @@ let type_of_apply env func funt argsv argstv =
   apply_rec 0 (inject funt)
 
 (* Type of primitive constructs *)
-let type_of_prim_type _env = function
-  | CPrimitives.PT_int63 -> Constr.mkSet
-  | CPrimitives.PT_float64 -> Constr.mkSet
+let type_of_prim_type _env u (type a) (prim : a CPrimitives.prim_type) = match prim with
+  | CPrimitives.PT_int63 ->
+    assert (Univ.Instance.is_empty u);
+    Constr.mkSet
+  | CPrimitives.PT_float64 ->
+    assert (Univ.Instance.is_empty u);
+    Constr.mkSet
+  | CPrimitives.PT_array ->
+    begin match Univ.Instance.to_array u with
+    | [|u|] ->
+      let ty = Constr.mkType (Univ.Universe.make u) in
+      Constr.mkProd(Context.anonR, ty , ty)
+    | _ -> anomaly Pp.(str"universe instance for array type should have length 1")
+    end
 
 let type_of_int env =
   match env.retroknowledge.Retroknowledge.retro_int63 with
@@ -228,71 +239,11 @@ let type_of_float env =
   | None -> raise
         (Invalid_argument "Typeops.type_of_float: float64 not_defined")
 
-let type_of_prim env t =
-  let int_ty () = type_of_int env in
-  let float_ty () = type_of_float env in
-  let bool_ty () =
-    match env.retroknowledge.Retroknowledge.retro_bool with
-    | Some ((ind,_),_) -> Constr.mkInd ind
-    | None -> CErrors.user_err Pp.(str"The type bool must be registered before this primitive.")
-  in
-  let compare_ty () =
-    match env.retroknowledge.Retroknowledge.retro_cmp with
-    | Some ((ind,_),_,_) -> Constr.mkInd ind
-    | None -> CErrors.user_err Pp.(str"The type compare must be registered before this primitive.")
-  in
-  let f_compare_ty () =
-    match env.retroknowledge.Retroknowledge.retro_f_cmp with
-    | Some ((ind,_),_,_,_) -> Constr.mkInd ind
-    | None -> CErrors.user_err Pp.(str"The type float_comparison must be registered before this primitive.")
-  in
-  let f_class_ty () =
-    match env.retroknowledge.Retroknowledge.retro_f_class with
-    | Some ((ind,_),_,_,_,_,_,_,_,_) -> Constr.mkInd ind
-    | None -> CErrors.user_err Pp.(str"The type float_class must be registered before this primitive.")
-  in
-  let pair_ty fst_ty snd_ty =
-    match env.retroknowledge.Retroknowledge.retro_pair with
-    | Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|])
-    | None -> CErrors.user_err Pp.(str"The type pair must be registered before this primitive.")
-  in
-  let carry_ty int_ty =
-    match env.retroknowledge.Retroknowledge.retro_carry with
-    | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|])
-    | None -> CErrors.user_err Pp.(str"The type carry must be registered before this primitive.")
-  in
-  let open CPrimitives in
-  let tr_prim_type = function
-    | PT_int63 -> int_ty ()
-    | PT_float64 -> float_ty () in
-  let tr_ind (type t) (i : t prim_ind) (a : t) = match i, a with
-    | PIT_bool, () -> bool_ty ()
-    | PIT_carry, t -> carry_ty (tr_prim_type t)
-    | PIT_pair, (t1, t2) -> pair_ty (tr_prim_type t1) (tr_prim_type t2)
-    | PIT_cmp, () -> compare_ty ()
-    | PIT_f_cmp, () -> f_compare_ty ()
-    | PIT_f_class, () -> f_class_ty () in
-  let tr_type = function
-    | PITT_ind (i, a) -> tr_ind i a
-    | PITT_type t -> tr_prim_type t in
-  let rec nary_op = function
-    | [] -> assert false
-    | [ret_ty] -> tr_type ret_ty
-    | arg_ty :: r ->
-       let arg_ty = tr_type arg_ty in
-       Constr.mkProd(Context.nameR (Id.of_string "x"), arg_ty, nary_op r) in
-  nary_op (types t)
-
-let type_of_prim_or_type env = let open CPrimitives in
-  function
-  | OT_type t -> type_of_prim_type env t
-  | OT_op op -> type_of_prim env op
-
-let judge_of_int env i =
-  make_judge (Constr.mkInt i) (type_of_int env)
-
-let judge_of_float env f =
-  make_judge (Constr.mkFloat f) (type_of_float env)
+let type_of_array env u =
+  assert (Univ.Instance.length u = 1);
+  match env.retroknowledge.Retroknowledge.retro_array with
+  | Some c -> mkConstU (c,u)
+  | None -> CErrors.user_err Pp.(str"The type array must be registered before this construction can be typechecked.")
 
 (* Type of product *)
 
@@ -354,6 +305,18 @@ let check_cast env c ct k expected_type =
   with NotConvertible ->
     error_actual_type env (make_judge c ct) expected_type
 
+let judge_of_int env i =
+  make_judge (Constr.mkInt i) (type_of_int env)
+
+let judge_of_float env f =
+  make_judge (Constr.mkFloat f) (type_of_float env)
+
+let judge_of_array env u tj defj =
+  let def = defj.uj_val in
+  let ty = defj.uj_type in
+  Array.iter (fun j -> check_cast env j.uj_val j.uj_type DEFAULTcast ty) tj;
+  make_judge (mkArray(u, Array.map j_val tj, def, ty)) (mkApp (type_of_array env u, [|ty|]))
+
 (* Inductive types. *)
 
 (* The type is parametric over the uniform parameters whose conclusion
@@ -621,6 +584,23 @@ let rec execute env cstr =
     (* Primitive types *)
     | Int _ -> cstr, type_of_int env
     | Float _ -> cstr, type_of_float env
+    | Array(u,t,def,ty) ->
+      (* ty : Type@{u} and all of t,def : ty *)
+      let ulev = match Univ.Instance.to_array u with
+        | [|u|] -> u
+        | _ -> assert false
+      in
+      let ty',tyty = execute env ty in
+      check_cast env ty' tyty DEFAULTcast (mkType (Universe.make ulev));
+      let def', def_ty = execute env def in
+      check_cast env def' def_ty DEFAULTcast ty';
+      let ta = type_of_array env u in
+      let t' = Array.Smart.map (fun x ->
+        let x', xt = execute env x in
+        check_cast env x' xt DEFAULTcast ty';
+        x') t in
+      let cstr = if def'==def && t'==t && ty'==ty then cstr else mkArray(u, t',def',ty') in
+      cstr, mkApp(ta, [|ty'|])
 
     (* Partial proofs: unsupported by the kernel *)
     | Meta _ ->
@@ -747,7 +727,77 @@ let judge_of_case env ci pj iv cj lfj =
 
 (* Building type of primitive operators and type *)
 
-let check_primitive_type env op_t t =
-  let inft = type_of_prim_or_type env op_t in
-  try default_conv ~l2r:false CUMUL env inft t
-  with NotConvertible -> error_incorrect_primitive env (make_judge op_t inft) t
+let type_of_prim_const env _u c =
+  let int_ty () = type_of_int env in
+  match c with
+  | CPrimitives.Arraymaxlength ->
+    int_ty ()
+
+let type_of_prim env u t =
+  let int_ty () = type_of_int env in
+  let float_ty () = type_of_float env in
+  let array_ty u a = mkApp(type_of_array env u, [|a|]) in
+  let bool_ty () =
+    match env.retroknowledge.Retroknowledge.retro_bool with
+    | Some ((ind,_),_) -> Constr.mkInd ind
+    | None -> CErrors.user_err Pp.(str"The type bool must be registered before this primitive.")
+  in
+  let compare_ty () =
+    match env.retroknowledge.Retroknowledge.retro_cmp with
+    | Some ((ind,_),_,_) -> Constr.mkInd ind
+    | None -> CErrors.user_err Pp.(str"The type compare must be registered before this primitive.")
+  in
+  let f_compare_ty () =
+    match env.retroknowledge.Retroknowledge.retro_f_cmp with
+    | Some ((ind,_),_,_,_) -> Constr.mkInd ind
+    | None -> CErrors.user_err Pp.(str"The type float_comparison must be registered before this primitive.")
+  in
+  let f_class_ty () =
+    match env.retroknowledge.Retroknowledge.retro_f_class with
+    | Some ((ind,_),_,_,_,_,_,_,_,_) -> Constr.mkInd ind
+    | None -> CErrors.user_err Pp.(str"The type float_class must be registered before this primitive.")
+  in
+  let pair_ty fst_ty snd_ty =
+    match env.retroknowledge.Retroknowledge.retro_pair with
+    | Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|])
+    | None -> CErrors.user_err Pp.(str"The type pair must be registered before this primitive.")
+  in
+  let carry_ty int_ty =
+    match env.retroknowledge.Retroknowledge.retro_carry with
+    | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|])
+    | None -> CErrors.user_err Pp.(str"The type carry must be registered before this primitive.")
+  in
+  let open CPrimitives in
+  let tr_prim_type (tr_type : ind_or_type -> constr) (type a) (ty : a prim_type) (t : a) = match ty with
+    | PT_int63 -> int_ty t
+    | PT_float64 -> float_ty t
+    | PT_array -> array_ty (fst t) (tr_type (snd t))
+  in
+  let tr_ind (tr_type : ind_or_type -> constr) (type t) (i : t prim_ind) (a : t) = match i, a with
+    | PIT_bool, () -> bool_ty ()
+    | PIT_carry, t -> carry_ty (tr_type t)
+    | PIT_pair, (t1, t2) -> pair_ty (tr_type t1) (tr_type t2)
+    | PIT_cmp, () -> compare_ty ()
+    | PIT_f_cmp, () -> f_compare_ty ()
+    | PIT_f_class, () -> f_class_ty ()
+  in
+  let rec tr_type n = function
+    | PITT_ind (i, a) -> tr_ind (tr_type n) i a
+    | PITT_type (ty,t) -> tr_prim_type (tr_type n) ty t
+    | PITT_param i -> Constr.mkRel (n+i)
+  in
+  let rec nary_op n = function
+    | [] -> assert false
+    | [ret_ty] -> tr_type n ret_ty
+    | arg_ty :: r ->
+      Constr.mkProd(Context.nameR (Id.of_string "x"), tr_type n arg_ty, nary_op (n+1) r)
+  in
+  let params, sign = types t in
+  assert (AUContext.size (univs t) = Instance.length u);
+  Vars.subst_instance_constr u (Term.it_mkProd_or_LetIn (nary_op 0 sign) params)
+
+let type_of_prim_or_type env u = let open CPrimitives in
+  function
+  | OT_type t -> type_of_prim_type env u t
+  | OT_op op -> type_of_prim env u op
+  | OT_const c -> type_of_prim_const env u c
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 65531ed38a..87a5666fcc 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -114,8 +114,6 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
 val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) ->
   GlobRef.t -> Constr.named_context -> unit
 
-val check_primitive_type : env -> CPrimitives.op_or_type -> types -> unit
-
 (** Types for primitives *)
 
 val type_of_int : env -> types
@@ -124,8 +122,12 @@ val judge_of_int : env -> Uint63.t -> unsafe_judgment
 val type_of_float : env -> types
 val judge_of_float : env -> Float64.t -> unsafe_judgment
 
-val type_of_prim_type : env -> CPrimitives.prim_type -> types
-val type_of_prim : env -> CPrimitives.t -> types
+val type_of_array : env -> Univ.Instance.t -> types
+val judge_of_array : env -> Univ.Instance.t -> unsafe_judgment array -> unsafe_judgment -> unsafe_judgment
+
+val type_of_prim_type : env -> Univ.Instance.t -> 'a CPrimitives.prim_type -> types
+val type_of_prim : env -> Univ.Instance.t -> CPrimitives.t -> types
+val type_of_prim_or_type : env -> Univ.Instance.t -> CPrimitives.op_or_type -> types
 
 val warn_bad_relevance_name : string
 (** Allow the checker to make this warning into an error. *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 0aca4b41ad..6d8aa02dff 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -985,6 +985,8 @@ module AUContext =
 struct
   type t = Names.Name.t array constrained
 
+  let make names csts : t = names, csts
+
   let repr (inst, cst) =
     (Array.init (Array.length inst) (fun i -> Level.var i), cst)
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 7651e34b12..7286fc84cb 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -353,6 +353,10 @@ module AUContext :
 sig
   type t
 
+  val make : Names.Name.t array -> Constraint.t -> t
+  (** Build an abstract context. Constraints may be between universe
+     variables. *)
+
   val repr : t -> UContext.t
   (** [repr ctx] is [(Var(0), ... Var(n-1) |= cstr] where [n] is the length of
       the context and [cstr] the abstracted Constraint.t. *)
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 63d88c659a..f7e28b0cfe 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -252,12 +252,22 @@ let subst_univs_level_constr subst c =
          let u' = Univ.subst_univs_level_universe subst u in
            if u' == u then t else
              (changed := true; mkSort (Sorts.sort_of_univ u'))
+
       | Case (ci,p,CaseInvert {univs;args},c,br) ->
         if Univ.Instance.is_empty univs then Constr.map aux t
         else
           let univs' = f univs in
           if univs' == univs then Constr.map aux t
           else (changed:=true; Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br)))
+
+      | Array (u,elems,def,ty) ->
+        let u' = f u in
+        let elems' = CArray.Smart.map aux elems in
+        let def' = aux def in
+        let ty' = aux ty in
+        if u == u' && elems == elems' && def == def' && ty == ty' then t
+        else (changed := true; mkArray (u',elems',def',ty'))
+
       | _ -> Constr.map aux t
     in
     let c' = aux c in
@@ -294,10 +304,20 @@ let subst_instance_constr subst c =
          let u' = Univ.subst_instance_universe subst u in
           if u' == u then t else
             (mkSort (Sorts.sort_of_univ u'))
+
       | Case (ci,p,CaseInvert {univs;args},c,br) ->
         let univs' = f univs in
         if univs' == univs then Constr.map aux t
         else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br))
+
+      | Array (u,elems,def,ty) ->
+        let u' = f u in
+        let elems' = CArray.Smart.map aux elems in
+        let def' = aux def in
+        let ty' = aux ty in
+        if u == u' && elems == elems' && def == def' && ty == ty' then t
+        else mkArray (u',elems',def',ty')
+
       | _ -> Constr.map aux t
     in
     aux c
@@ -319,11 +339,14 @@ let universes_of_constr c =
   let rec aux s c =
     match kind c with
     | Const (_c, u) ->
-       LSet.fold LSet.add (Instance.levels u) s
+      LSet.fold LSet.add (Instance.levels u) s
     | Ind ((_mind,_), u) | Construct (((_mind,_),_), u) ->
-       LSet.fold LSet.add (Instance.levels u) s
+      LSet.fold LSet.add (Instance.levels u) s
     | Sort u when not (Sorts.is_small u) ->
       let u = Sorts.univ_of_sort u in
       LSet.fold LSet.add (Universe.levels u) s
+    | Array (u,_,_,_) ->
+      let s = LSet.fold LSet.add (Instance.levels u) s in
+      Constr.fold aux s c
     | _ -> Constr.fold aux s c
   in aux LSet.empty c
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 3563407f7e..f78f0d4d1e 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -76,6 +76,11 @@ and conv_whd env pb k whd1 whd2 cu =
   | Vfloat64 f1, Vfloat64 f2 ->
     if Float64.(equal (of_float f1) (of_float f2)) then cu
     else raise NotConvertible
+  | Varray t1, Varray t2 ->
+    if t1 == t2 then cu else
+    let n = Parray.length_int t1 in
+    if not (Int.equal n (Parray.length_int t2)) then raise NotConvertible;
+    Parray.fold_left2 (fun cu v1 v2 -> conv_val env CONV k v1 v2 cu) cu t1 t2
   | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) ->
       conv_atom env pb k a1 stk1 a2 stk2 cu
   | Vfun _, _ | _, Vfun _ ->
@@ -83,7 +88,7 @@ and conv_whd env pb k whd1 whd2 cu =
       conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu
 
   | Vprod _, _ | Vfix _, _ | Vcofix _, _  | Vconstr_const _, _ | Vint64 _, _
-  | Vfloat64 _, _ | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible
+  | Vfloat64 _, _ | Varray _, _ | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible
 
 
 and conv_atom env pb k a1 stk1 a2 stk2 cu =
diff --git a/kernel/vm.ml b/kernel/vm.ml
index f2d033f89b..d8c66bebd2 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -169,7 +169,7 @@ let rec apply_stack a stk v =
 let apply_whd k whd =
   let v = val_of_rel k in
   match whd with
-  | Vprod _ | Vconstr_const _ | Vconstr_block _ | Vint64 _ | Vfloat64 _ ->
+  | Vprod _ | Vconstr_const _ | Vconstr_block _ | Vint64 _ | Vfloat64 _ | Varray _ ->
      assert false
   | Vfun f -> reduce_fun k f
   | Vfix(f, None) ->
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index f4ce953d4a..ec429d5f9e 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -292,6 +292,7 @@ type whd =
   | Vconstr_block of vblock
   | Vint64 of int64
   | Vfloat64 of float
+  | Varray of values Parray.t
   | Vatom_stk of atom * stack
   | Vuniv_level of Univ.Level.t
 
@@ -324,6 +325,7 @@ let uni_lvl_val (v : values) : Univ.Level.t =
         | Vconstr_block _b -> str "Vconstr_block"
         | Vint64 _ -> str "Vint64"
         | Vfloat64 _ -> str "Vfloat64"
+        | Varray _ -> str "Varray"
         | Vatom_stk (_a,_stk) -> str "Vatom_stk"
         | Vuniv_level _ -> assert false
       in
@@ -403,7 +405,9 @@ let whd_val : values -> whd =
     else
       let tag = Obj.tag o in
       if tag = accu_tag then
-        if is_accumulate (fun_code o) then whd_accu o []
+        if Int.equal (Obj.size o) 1 then
+          Varray(Obj.obj o)
+        else if is_accumulate (fun_code o) then whd_accu o []
         else Vprod(Obj.obj o)
       else
         if tag = Obj.closure_tag || tag = Obj.infix_tag then
@@ -456,7 +460,9 @@ let val_of_atom a = val_of_obj (obj_of_atom a)
 
 let val_of_int i = (Obj.magic i : values)
 
-let val_of_uint i = (Obj.magic i : values)
+let val_of_uint i = (Obj.magic i : structured_values)
+
+let val_of_parray p = (Obj.magic p : structured_values)
 
 let atom_of_proj kn v =
   let r = Obj.new_block proj_tag 2 in
@@ -689,6 +695,7 @@ and pr_whd w =
   | Vconstr_block _b -> str "Vconstr_block"
   | Vint64 i -> i |> Format.sprintf "Vint64(%LiL)" |> str
   | Vfloat64 f -> str "Vfloat64(" ++ str (Float64.(to_string (of_float f))) ++ str ")"
+  | Varray _ -> str "Varray"
   | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")"
   | Vuniv_level _ -> assert false)
 and pr_stack stk =
@@ -701,3 +708,13 @@ and pr_zipper z =
   | Zfix (_f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")"
   | Zswitch _s -> str "Zswitch(...)"
   | Zproj c -> str "Zproj(" ++ Projection.Repr.print c ++ str ")")
+
+(** Primitives implemented in OCaml *)
+
+let parray_make = Obj.magic Parray.make
+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 cd85440fed..f4070a02a3 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -129,6 +129,7 @@ type whd =
   | Vconstr_block of vblock
   | Vint64 of int64
   | Vfloat64 of float
+  | Varray of values Parray.t
   | Vatom_stk of atom * stack
   | Vuniv_level of Univ.Level.t
 
@@ -150,6 +151,7 @@ val val_of_atom : atom -> values
 val val_of_int : int -> structured_values
 val val_of_block : tag -> structured_values array -> structured_values
 val val_of_uint : Uint63.t -> structured_values
+val val_of_parray : structured_values Parray.t -> structured_values
 
 external val_of_annot_switch : annot_switch -> values = "%identity"
 external val_of_proj_name : Projection.Repr.t -> values = "%identity"
@@ -199,3 +201,12 @@ val bfield : vblock -> int -> values
 
 val check_switch : vswitch -> vswitch -> bool
 val branch_arg : int -> tag * int -> values
+
+(** Primitives implemented in OCaml, seen as values (to be used as globals) *)
+val parray_make : values
+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
author	Maxime Dénès	2020-02-03 18:19:42 +0100
committer	Maxime Dénès	2020-07-06 11:22:43 +0200
commit	0ea2d0ff4ed84e1cc544c958b8f6e98f6ba2e9b6 (patch)
tree	fbad060c3c2e29e81751dea414c898b5cb0fa22d /kernel
parent	cf388fdb679adb88a7e8b3122f65377552d2fb94 (diff)