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>

23 files changed, 329 insertions, 80 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index b713d7812e..2c7b689c04 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -52,7 +52,8 @@ type cbv_value =
   | FIXP of fixpoint * cbv_value subs * cbv_value array
   | COFIXP of cofixpoint * cbv_value subs * cbv_value array
   | CONSTR of constructor Univ.puniverses * cbv_value array
-  | PRIMITIVE of CPrimitives.t * constr * cbv_value array
+  | PRIMITIVE of CPrimitives.t * pconstant * cbv_value array
+  | ARRAY of Univ.Instance.t * cbv_value Parray.t * cbv_value
 
 (* type of terms with a hole. This hole can appear only under App or Case.
  *   TOP means the term is considered without context
@@ -98,6 +99,8 @@ let rec shift_value n = function
       CONSTR (c, Array.map (shift_value n) args)
   | PRIMITIVE(op,c,args) ->
       PRIMITIVE(op,c,Array.map (shift_value n) args)
+  | ARRAY (u,t,ty) ->
+      ARRAY(u, Parray.map (shift_value n) t, shift_value n ty)
 
 let shift_value n v =
   if Int.equal n 0 then v else shift_value n v
@@ -170,7 +173,7 @@ let strip_appl head stack =
     | COFIXP (cofix,env,app) -> (COFIXP(cofix,env,[||]), stack_app app stack)
     | CONSTR (c,app) -> (CONSTR(c,[||]), stack_app app stack)
     | PRIMITIVE(op,c,app) -> (PRIMITIVE(op,c,[||]), stack_app app stack)
-    | VAL _ | STACK _ | CBN _ | LAM _ -> (head, stack)
+    | VAL _ | STACK _ | CBN _ | LAM _ | ARRAY _ -> (head, stack)
 
 
 (* Tests if fixpoint reduction is possible. *)
@@ -209,6 +212,7 @@ module VNativeEntries =
     type elem = cbv_value
     type args = cbv_value array
     type evd = unit
+    type uinstance = Univ.Instance.t
 
     let get = Array.get
 
@@ -228,6 +232,11 @@ module VNativeEntries =
         | _ -> raise Primred.NativeDestKO)
       | _ -> raise Primred.NativeDestKO
 
+    let get_parray () e =
+      match e with
+      | ARRAY(_u,t,_ty) -> t
+      | _ -> raise Primred.NativeDestKO
+
     let mkInt env i = VAL(0, mkInt i)
 
     let mkFloat env f = VAL(0, mkFloat f)
@@ -327,6 +336,9 @@ module VNativeEntries =
       let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,nan) =
         get_f_class_constructors env in
       CONSTR(Univ.in_punivs nan, [||])
+
+    let mkArray env u t ty =
+      ARRAY (u,t,ty)
   end
 
 module VredNative = RedNative(VNativeEntries)
@@ -368,7 +380,10 @@ and reify_value = function (* reduction under binders *)
   | CONSTR (c,args) ->
       mkApp(mkConstructU c, Array.map reify_value args)
   | PRIMITIVE(op,c,args) ->
-      mkApp(c, Array.map reify_value args)
+      mkApp(mkConstU c, Array.map reify_value args)
+  | ARRAY (u,t,ty) ->
+    let t, def = Parray.to_array t in
+      mkArray(u, Array.map reify_value t, reify_value def, reify_value ty)
 
 and apply_env env t =
   match kind t with
@@ -458,6 +473,15 @@ let rec norm_head info env t stack =
   | CoFix cofix -> (COFIXP(cofix,env,[||]), stack)
   | Construct c -> (CONSTR(c, [||]), stack)
 
+  | Array(u,t,def,ty) ->
+    let ty = cbv_stack_term info TOP env ty in
+    let len = Array.length t in
+    let t =
+      Parray.init (Uint63.of_int len)
+      (fun i -> cbv_stack_term info TOP env t.(i))
+      (cbv_stack_term info TOP env def) in
+    (ARRAY (u,t,ty), stack)
+
   (* neutral cases *)
   | (Sort _ | Meta _ | Ind _ | Int _ | Float _) -> (VAL(0, t), stack)
   | Prod _ -> (CBN(t,env), stack)
@@ -468,7 +492,12 @@ and norm_head_ref k info env stack normt t =
       | Declarations.Def body ->
          if get_debug_cbv () then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt);
          strip_appl (shift_value k body) stack
-      | Declarations.Primitive op -> (PRIMITIVE(op,t,[||]),stack)
+      | Declarations.Primitive op ->
+        let c = match normt with
+          | ConstKey c -> c
+          | RelKey _ | VarKey _ -> assert false
+        in
+        (PRIMITIVE(op,c,[||]),stack)
       | Declarations.OpaqueDef _ | Declarations.Undef _ ->
          if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt);
          (VAL(0,make_constr_ref k normt t),stack)
@@ -538,7 +567,7 @@ and cbv_stack_value info env = function
     | (CONSTR(c,[||]), APP(appl,TOP)) -> CONSTR(c,appl)
 
     (* primitive apply to arguments *)
-    | (PRIMITIVE(op,c,[||]), APP(appl,stk)) ->
+    | (PRIMITIVE(op,(_,u as c),[||]), APP(appl,stk)) ->
       let nargs = CPrimitives.arity op in
       let len = Array.length appl in
       if nargs <= len then
@@ -549,7 +578,7 @@ and cbv_stack_value info env = function
           if nargs < len then
             stack_app (Array.sub appl nargs (len - nargs)) stk
           else stk in
-        match VredNative.red_prim info.env () op args with
+        match VredNative.red_prim info.env () op u args with
         | Some (CONSTR (c, args)) ->
           (* args must be moved to the stack to allow future reductions *)
           cbv_stack_value info env (CONSTR(c, [||]), stack_app args stk)
@@ -585,7 +614,7 @@ and cbv_value_cache info ref =
         let v = cbv_stack_term info TOP (subs_id 0) body in
         Declarations.Def v
       with
-      | Environ.NotEvaluableConst (Environ.IsPrimitive op) -> Declarations.Primitive op
+      | Environ.NotEvaluableConst (Environ.IsPrimitive (_u,op)) -> Declarations.Primitive op
       | Not_found | Environ.NotEvaluableConst _ -> Declarations.Undef None
     in
     KeyTable.add info.tab ref v; v
@@ -643,7 +672,12 @@ and cbv_norm_value info = function (* reduction under binders *)
   | CONSTR (c,args) ->
       mkApp(mkConstructU c, Array.map (cbv_norm_value info) args)
   | PRIMITIVE(op,c,args) ->
-      mkApp(c,Array.map (cbv_norm_value info) args)
+      mkApp(mkConstU c,Array.map (cbv_norm_value info) args)
+  | ARRAY (u,t,ty) ->
+    let ty = cbv_norm_value info ty in
+    let t, def = Parray.to_array t in
+    let def = cbv_norm_value info def in
+      mkArray(u, Array.map (cbv_norm_value info) t, def, ty)
 
 (* with profiling *)
 let cbv_norm infos constr =
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index d7804edf6d..409f4c0f70 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -36,7 +36,8 @@ type cbv_value =
   | FIXP of fixpoint * cbv_value subs * cbv_value array
   | COFIXP of cofixpoint * cbv_value subs * cbv_value array
   | CONSTR of constructor Univ.puniverses * cbv_value array
-  | PRIMITIVE of CPrimitives.t * Constr.t * cbv_value array
+  | PRIMITIVE of CPrimitives.t * pconstant * cbv_value array
+  | ARRAY of Univ.Instance.t * cbv_value Parray.t * cbv_value
 
 and cbv_stack =
   | TOP
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 656739657d..419eeaa92a 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -406,10 +406,16 @@ let matches_core env sigma allow_bound_rels
       | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 ->
          List.fold_left2 (sorec ctx env) subst args1 args2
       | PInt i1, Int i2 when Uint63.equal i1 i2 -> subst
+
       | PFloat f1, Float f2 when Float64.equal f1 f2 -> subst
+
+      | PArray(pt,pdef,pty), Array(_u,t,def,ty)
+             when Array.length pt = Array.length t ->
+         sorec ctx env (sorec ctx env (Array.fold_left2 (sorec ctx env) subst pt t) pdef def) pty ty
+
       | (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _
          | PProd _ | PLetIn _ | PSort _ | PIf _ | PCase _
-         | PFix _ | PCoFix _| PEvar _ | PInt _ | PFloat _), _ -> raise PatternMatchingFailure
+         | PFix _ | PCoFix _| PEvar _ | PInt _ | PFloat _ | PArray _), _ -> raise PatternMatchingFailure
 
   in
   sorec [] env ((Id.Map.empty,Id.Set.empty), Id.Map.empty) pat c
@@ -527,6 +533,13 @@ let sub_match ?(closed=true) env sigma pat c =
       aux env term mk_ctx next
     with Retyping.RetypeError _ -> next ()
     end
+  | Array(u, t, def, ty) ->
+    let next_mk_ctx = function
+    | def :: ty :: l -> mk_ctx (mkArray(u, Array.of_list l, def, ty))
+    | _ -> assert false
+    in
+    let sub = (env,def) :: (env,ty) :: subargs env t in
+    try_aux sub next_mk_ctx next
   | Construct _|Ind _|Evar _|Const _|Rel _|Meta _|Var _|Sort _|Int _|Float _ ->
     next ()
   in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 02c04c2300..7fcb0795bd 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -809,6 +809,12 @@ and detype_r d flags avoid env sigma t =
     | CoFix (n,recdef) -> detype_cofix (detype d) flags avoid env sigma n recdef
     | Int i -> GInt i
     | Float f -> GFloat f
+    | Array(u,t,def,ty) ->
+      let t = Array.map (detype d flags avoid env sigma) t in
+      let def = detype d flags avoid env sigma def in
+      let ty = detype d flags avoid env sigma ty in
+      let u = detype_instance sigma u in
+      GArray(u, t, def, ty)
 
 and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl =
   try
@@ -1096,6 +1102,14 @@ let rec subst_glob_constr env subst = DAst.map (function
       let k' = smartmap_cast_type (subst_glob_constr env subst) k in
       if r1' == r1 && k' == k then raw else GCast (r1',k')
 
+  | GArray (u,t,def,ty) as raw ->
+      let def' = subst_glob_constr env subst def
+      and t' = Array.Smart.map (subst_glob_constr env subst) t
+      and ty' = subst_glob_constr env subst ty
+      in
+        if def' == def && t' == t && ty' == ty then raw else
+          GArray(u,t',def',ty')
+
   )
 
 (* Utilities to transform kernel cases to simple pattern-matching problem *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0206d4e70d..6880383a31 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -130,7 +130,7 @@ let flex_kind_of_term flags env evd c sk =
     | Evar ev ->
        if is_frozen flags ev then Rigid
        else Flexible ev
-    | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ | Float _ -> Rigid
+    | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> Rigid
     | Meta _ -> Rigid
     | Fix _ -> Rigid (* happens when the fixpoint is partially applied *)
     | Cast _ | App _ | Case _ -> assert false
@@ -212,7 +212,7 @@ let occur_rigidly flags env evd (evk,_) t =
       (match aux c with
       | Rigid b -> Rigid b
       | _ -> Reducible)
-    | Meta _ | Fix _ | CoFix _ | Int _ | Float _ -> Reducible
+    | Meta _ | Fix _ | CoFix _ | Int _ | Float _ | Array _ -> Reducible
   in
     match aux t with
     | Rigid b -> b
@@ -898,7 +898,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
              only if necessary) or the second argument is potentially
              usable as a canonical projection or canonical value *)
           let rec is_unnamed (hd, args) = match EConstr.kind i hd with
-            | (Var _|Construct _|Ind _|Const _|Prod _|Sort _|Int _ |Float _) ->
+            | (Var _|Construct _|Ind _|Const _|Prod _|Sort _|Int _ |Float _|Array _) ->
               Stack.not_purely_applicative args
             | (CoFix _|Meta _|Rel _)-> true
             | Evar _ -> Stack.not_purely_applicative args
@@ -1019,7 +1019,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
         | Ind _, Ind _
         | Construct _, Construct _
         | Int _, Int _
-        | Float _, Float _ ->
+        | Float _, Float _
+        | Array _, Array _ ->
           rigids env evd sk1 term1 sk2 term2
 
         | Evar (sp1,al1), Evar (sp2,al2) -> (* Frozen evars *)
@@ -1064,9 +1065,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
           |Some (sk1',sk2'), Success i' -> evar_conv_x flags env i' CONV (Stack.zip i' (term1,sk1')) (Stack.zip i' (term2,sk2'))
           end
 
-        | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Float _ | Evar _ | Lambda _), _ ->
+        | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Float _ | Array _ | Evar _ | Lambda _), _ ->
           UnifFailure (evd,NotSameHead)
-        | _, (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Evar _ | Lambda _) ->
+        | _, (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Array _ | Evar _ | Lambda _) ->
           UnifFailure (evd,NotSameHead)
         | Case _, _ -> UnifFailure (evd,NotSameHead)
         | Proj _, _ -> UnifFailure (evd,NotSameHead)
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 71edcaa231..f33030d6a4 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -180,26 +180,71 @@ let define_evar_as_sort env evd (ev,args) =
    constraint on its domain and codomain. If the input constraint is
    an evar instantiate it with the product of 2 new evars. *)
 
+let rec presplit env sigma c =
+  let c = Reductionops.whd_all env sigma c in
+  match EConstr.kind sigma c with
+  | App (h,args) when isEvar sigma h ->
+    let sigma, lam = define_evar_as_lambda env sigma (destEvar sigma h) in
+    (* XXX could be just whd_all -> no recursion? *)
+    presplit env sigma (mkApp (lam, args))
+  | _ -> sigma, c
+
 let split_tycon ?loc env evd tycon =
-  let rec real_split evd c =
-    let t = Reductionops.whd_all env evd c in
-      match EConstr.kind evd t with
-        | Prod (na,dom,rng) -> evd, (na, dom, rng)
-        | Evar ev (* ev is undefined because of whd_all *) ->
-            let (evd',prod) = define_evar_as_product env evd ev in
-            let (na,dom,rng) = destProd evd prod in
-            let anon = {na with binder_name = Anonymous} in
-              evd',(anon, dom, rng)
-        | App (c,args) when isEvar evd c ->
-            let (evd',lam) = define_evar_as_lambda env evd (destEvar evd c) in
-            real_split evd' (mkApp (lam,args))
-        | _ -> error_not_product ?loc env evd c
-  in
-    match tycon with
-      | None -> evd,(make_annot Anonymous Relevant,None,None)
-      | Some c ->
-          let evd', (n, dom, rng) = real_split evd c in
-            evd', (n, mk_tycon dom, mk_tycon rng)
+  match tycon with
+  | None -> evd,(make_annot Anonymous Relevant,None,None)
+  | Some c ->
+    let evd, c = presplit env evd c in
+    let evd, na, dom, rng = match EConstr.kind evd c with
+      | Prod (na,dom,rng) -> evd, na, dom, rng
+      | Evar ev ->
+        let (evd,prod) = define_evar_as_product env evd ev in
+        let (na,dom,rng) = destProd evd prod in
+        let anon = {na with binder_name = Anonymous} in
+        evd, anon, dom, rng
+      | _ ->
+        (* XXX no error to allow later coercion? Not sure if possible with funclass *)
+        error_not_product ?loc env evd c
+    in
+    evd, (na, mk_tycon dom, mk_tycon rng)
+
+
+let define_pure_evar_as_array env sigma evk =
+  let evi = Evd.find_undefined sigma evk in
+  let evenv = evar_env env evi in
+  let evksrc = evar_source evk sigma in
+  let src = subterm_source evk ~where:Domain evksrc in
+  let sigma, (ty,u) = new_type_evar evenv sigma univ_flexible ~src ~filter:(evar_filter evi) in
+  let concl = Reductionops.whd_all evenv sigma evi.evar_concl in
+  let s = destSort sigma concl in
+  (* array@{u} ty : Type@{u} <= Type@{s} *)
+  let sigma = Evd.set_leq_sort env sigma u (ESorts.kind sigma s) in
+  let u = Option.get (Univ.Universe.level (Sorts.univ_of_sort u)) in
+  let ar = Typeops.type_of_array env (Univ.Instance.of_array [|u|]) in
+  let sigma = Evd.define evk (mkApp (EConstr.of_constr ar, [| ty |])) sigma in
+  sigma
+
+let is_array_const env sigma c =
+  match EConstr.kind sigma c with
+  | Const (cst,_) ->
+    (match env.Environ.retroknowledge.Retroknowledge.retro_array with
+     | None -> false
+     | Some cst' -> Constant.equal cst cst')
+  | _ -> false
+
+let split_as_array env sigma0 = function
+  | None -> sigma0, None
+  | Some c ->
+    let sigma, c = presplit env sigma0 c in
+    match EConstr.kind sigma c with
+    | App (h,[|ty|]) when is_array_const env sigma h -> sigma, Some ty
+    | Evar ev ->
+      let sigma = define_pure_evar_as_array env sigma (fst ev) in
+      let ty = match EConstr.kind sigma c with
+        | App (_,[|ty|]) -> ty
+        | _ -> assert false
+      in
+      sigma, Some ty
+    | _ -> sigma0, None
 
 let valcon_of_tycon x = x
 let lift_tycon n = Option.map (lift n)
diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli
index a4169c2298..e5c3f8baa1 100644
--- a/pretyping/evardefine.mli
+++ b/pretyping/evardefine.mli
@@ -35,6 +35,11 @@ val split_tycon :
   ?loc:Loc.t -> env ->  evar_map -> type_constraint ->
     evar_map * (Name.t Context.binder_annot * type_constraint * type_constraint)
 
+val split_as_array : env -> evar_map -> type_constraint ->
+  evar_map * type_constraint
+(** If the constraint can be made to look like [array A] return [A],
+   otherwise return [None] (this makes later coercion possible). *)
+
 val valcon_of_tycon : type_constraint -> val_constraint
 val lift_tycon : int -> type_constraint -> type_constraint
 
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 342175a512..5bd26be823 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -168,9 +168,12 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
     f c1 c2 && cast_type_eq f t1 t2
   | GInt i1, GInt i2 -> Uint63.equal i1 i2
   | GFloat f1, GFloat f2 -> Float64.equal f1 f2
+  | GArray (u1, t1, def1, ty1), GArray (u2, t2, def2, ty2) ->
+    Array.equal f t1 t2 && f def1 def2 && f ty1 ty2 &&
+    Option.equal (List.equal glob_level_eq) u1 u2
   | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ |
      GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ |
-     GInt _ | GFloat _), _ -> false
+     GInt _ | GFloat _ | GArray _), _ -> false
 
 let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c
 
@@ -231,6 +234,11 @@ let map_glob_constr_left_to_right f = DAst.map (function
       let comp1 = f c in
       let comp2 = map_cast_type f k in
       GCast (comp1,comp2)
+  | GArray (u,t,def,ty) ->
+      let comp1 = Array.map_left f t in
+      let comp2 = f def in
+      let comp3 = f ty in
+      GArray (u,comp1,comp2,comp3)
   | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) as x -> x
   )
 
@@ -263,6 +271,7 @@ let fold_glob_constr f acc = DAst.with_val (function
     let acc = match k with
       | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in
     f acc c
+  | GArray (_u,t,def,ty) -> f (f (Array.fold_left f acc t) def) ty
   | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc
   )
 let fold_return_type_with_binders f g v acc (na,tyopt) =
@@ -305,6 +314,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
     let acc = match k with
       | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in
     f v acc c
+  | GArray (_u, t, def, ty) -> f v (f v (Array.fold_left (f v) acc t) def) ty
   | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc))
 
 let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index bccc30ad62..526eac6f1e 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -92,6 +92,7 @@ type 'a glob_constr_r =
   | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type
   | GInt of Uint63.t
   | GFloat of Float64.t
+  | GArray of glob_level list option * 'a glob_constr_g array * 'a glob_constr_g * 'a glob_constr_g
 and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t
 
 and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g
diff --git a/pretyping/heads.ml b/pretyping/heads.ml
index 98cfbf7fa7..d1ac0862ed 100644
--- a/pretyping/heads.ml
+++ b/pretyping/heads.ml
@@ -79,7 +79,7 @@ and kind_of_head env t =
   | Proj (p,c) -> RigidHead RigidOther
 
   | Case (_,_,_,c,_) -> aux k [] c true
-  | Int _ | Float _ -> ConstructorHead
+  | Int _ | Float _ | Array _ -> ConstructorHead
   | Fix ((i,j),_) ->
       let n = i.(j) in
       try aux k [] (List.nth l n) true
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 0e7fac35f1..5be8f9f83c 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -207,7 +207,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
               | ra::rest ->
                   (match dest_recarg ra with
                     | Mrec (_,j) when is_rec -> (depPvect.(j),rest)
-                    | Imbr _  -> (None,rest)
+                    | Nested _  -> (None,rest)
                     | _ -> (None, rest))
           in
           (match optionpos with
@@ -280,7 +280,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
         let optionpos =
           match dest_recarg recarg with
             | Norec   -> None
-            | Imbr _  -> None
+            | Nested _  -> None
             | Mrec (_,i)  -> fvect.(i)
         in
         (match optionpos with
diff --git a/pretyping/keys.ml b/pretyping/keys.ml
index 1e4f2f2340..7a7099c195 100644
--- a/pretyping/keys.ml
+++ b/pretyping/keys.ml
@@ -27,6 +27,7 @@ type key =
   | KRel
   | KInt
   | KFloat
+  | KArray
 
 module KeyOrdered = struct
   type t = key
@@ -44,6 +45,7 @@ module KeyOrdered = struct
     | KRel -> 7
     | KInt -> 8
     | KFloat -> 9
+    | KArray -> 10
 
   let compare gr1 gr2 =
     match gr1, gr2 with
@@ -138,6 +140,7 @@ let constr_key kind c =
       | LetIn _ -> KLet
       | Int _ -> KInt
       | Float _ -> KFloat
+      | Array _ -> KArray
     in Some (aux c)
   with Not_found -> None
 
@@ -155,6 +158,7 @@ let pr_key pr_global = function
   | KRel -> str"Rel"
   | KInt -> str"Int"
   | KFloat -> str"Float"
+  | KArray -> str"Array"
 
 let pr_keyset pr_global v =
   prlist_with_sep spc (pr_key pr_global) (Keyset.elements v)
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 89bd7e196f..30e1dc0611 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -214,6 +214,7 @@ let rec nf_val env sigma v typ =
   | Vconst n -> construct_of_constr_const env sigma n typ
   | Vint64 i -> i |> Uint63.of_int64 |> mkInt
   | Vfloat64 f -> f |> Float64.of_float |> mkFloat
+  | Varray t -> nf_array env sigma t typ
   | Vblock b ->
       let capp,ctyp = construct_of_constr_block env sigma (block_tag b) typ in
       let args = nf_bargs env sigma b ctyp in
@@ -442,6 +443,14 @@ and nf_evar env sigma evk args =
        evar node *)
     mkEvar (evk, List.rev args), ty
 
+and nf_array env sigma t typ =
+  let ty, allargs = app_type env typ in
+  let typ_elem = allargs.(0) in
+  let t, vdef = Parray.to_array t in
+  let t = Array.map (fun v -> nf_val env sigma v typ_elem) t in
+  let u = snd (destConst ty) in
+  mkArray(u, t, nf_val env sigma vdef typ_elem, typ_elem)
+
 let evars_of_evar_map sigma =
   { Nativelambda.evars_val = Evd.existential_opt_value0 sigma;
     Nativelambda.evars_metas = Evd.meta_type0 sigma }
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 1dfb8b2cd1..f6d61f4892 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -41,6 +41,7 @@ type constr_pattern =
   | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array)
   | PInt of Uint63.t
   | PFloat of Float64.t
+  | PArray of constr_pattern array * constr_pattern * constr_pattern
 
 (** Nota : in a [PCase], the array of branches might be shorter than
     expected, denoting the use of a final "_ => _" branch *)
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 4aedeb43e3..8c3d624f0f 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -64,10 +64,13 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
    Uint63.equal i1 i2
 | PFloat f1, PFloat f2 ->
    Float64.equal f1 f2
+| PArray (t1, def1, ty1), PArray (t2, def2, ty2) ->
+  Array.equal constr_pattern_eq t1 t2 && constr_pattern_eq def1 def2
+  && constr_pattern_eq ty1 ty2
 | (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _
    | PLambda _ | PProd _ | PLetIn _ | PSort _ | PMeta _
    | PIf _ | PCase _ | PFix _ | PCoFix _ | PProj _ | PInt _
-   | PFloat _), _ -> false
+   | PFloat _ | PArray _), _ -> false
 (** FIXME: fixpoint and cofixpoint should be relativized to pattern *)
 
 and pattern_eq (i1, j1, p1) (i2, j2, p2) =
@@ -93,6 +96,8 @@ let rec occur_meta_pattern = function
       (occur_meta_pattern p) ||
       (occur_meta_pattern c) ||
       (List.exists (fun (_,_,p) -> occur_meta_pattern p) br)
+  | PArray (t,def,ty) ->
+      Array.exists occur_meta_pattern t || occur_meta_pattern def || occur_meta_pattern ty
   | PMeta _ | PSoApp _ -> true
   | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _
     | PInt _ | PFloat _ -> false
@@ -121,6 +126,8 @@ let rec occurn_pattern n = function
      Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl
   | PCoFix (_,(_,tl,bl)) ->
      Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl
+  | PArray (t,def,ty) ->
+    Array.exists (occurn_pattern n) t || occurn_pattern n def || occurn_pattern n ty
 
 let noccurn_pattern n c = not (occurn_pattern n c)
 
@@ -139,7 +146,8 @@ let rec head_pattern_bound t =
         -> raise BoundPattern
     (* Perhaps they were arguments, but we don't beta-reduce *)
     | PLambda _ -> raise BoundPattern
-    | PCoFix _ | PInt _ | PFloat _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.")
+    | PCoFix _ | PInt _ | PFloat _ | PArray _ ->
+      anomaly ~label:"head_pattern_bound" (Pp.str "not a type.")
 
 let head_of_constr_reference sigma c = match EConstr.kind sigma c with
   | Const (sp,_) -> GlobRef.ConstRef sp
@@ -217,7 +225,10 @@ let pattern_of_constr env sigma t =
        PCoFix (ln,(Array.map binder_name lna,Array.map (pattern_of_constr env) tl,
                   Array.map (pattern_of_constr env') bl))
     | Int i -> PInt i
-    | Float f -> PFloat f in
+    | Float f -> PFloat f
+    | Array (_u, t, def, ty) ->
+      PArray (Array.map (pattern_of_constr env) t, pattern_of_constr env def, pattern_of_constr env ty)
+    in
   pattern_of_constr env t
 
 (* To process patterns, we need a translation without typing at all. *)
@@ -238,6 +249,7 @@ let map_pattern_with_binders g f l = function
   | PCoFix (ln,(lna,tl,bl)) ->
      let l' = Array.fold_left (fun l na -> g na l) l lna in
      PCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
+  | PArray (t,def,ty) -> PArray (Array.map (f l) t, f l def, f l ty)
   (* Non recursive *)
   | (PVar _ | PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _ | PInt _
      | PFloat _ as x) -> x
@@ -359,6 +371,12 @@ let rec subst_pattern env sigma subst pat =
       let bl' = Array.Smart.map (subst_pattern env sigma subst) bl in
       if bl' == bl && tl' == tl then pat
       else PCoFix (ln,(lna,tl',bl'))
+  | PArray (t,def,ty) ->
+      let t' = Array.Smart.map (subst_pattern env sigma subst) t in
+      let def' = subst_pattern env sigma subst def in
+      let ty' = subst_pattern env sigma subst ty in
+      if def' == def && t' == t && ty' == ty then pat
+      else PArray (t',def',ty')
 
 let mkPLetIn na b t c = PLetIn(na,b,t,c)
 let mkPProd na t u = PProd(na,t,u)
@@ -502,7 +520,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
 
   | GInt i -> PInt i
   | GFloat f -> PFloat f
-  | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ ->
+  | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GArray _ ->
       err ?loc (Pp.str "Non supported pattern."))
 
 and pat_of_glob_in_context metas vars decls c =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e4403d5bf4..b9825b6a92 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -508,6 +508,7 @@ type pretyper = {
   pretype_cast : pretyper -> glob_constr * glob_constr cast_type -> unsafe_judgment pretype_fun;
   pretype_int : pretyper -> Uint63.t -> unsafe_judgment pretype_fun;
   pretype_float : pretyper -> Float64.t -> unsafe_judgment pretype_fun;
+  pretype_array : pretyper -> glob_level list option * glob_constr array * glob_constr * glob_constr -> unsafe_judgment pretype_fun;
   pretype_type : pretyper -> glob_constr -> unsafe_type_judgment pretype_fun;
 }
 
@@ -549,6 +550,8 @@ let eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma t =
     self.pretype_int self n ?loc ~program_mode ~poly resolve_tc tycon env sigma
   | GFloat f ->
     self.pretype_float self f ?loc ~program_mode ~poly resolve_tc tycon env sigma
+  | GArray (u,t,def,ty) ->
+    self.pretype_array self (u,t,def,ty) ?loc ~program_mode ~poly resolve_tc tycon env sigma
 
 let eval_type_pretyper self ~program_mode ~poly resolve_tc tycon env sigma t =
   self.pretype_type self t ~program_mode ~poly resolve_tc tycon env sigma
@@ -1196,24 +1199,6 @@ struct
         sigma, { uj_val = v; uj_type = tval }
     in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon
 
-  let pretype_int self i =
-    fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
-        let resj =
-          try Typing.judge_of_int !!env i
-          with Invalid_argument _ ->
-            user_err ?loc ~hdr:"pretype" (str "Type of int63 should be registered first.")
-        in
-        discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
-
-  let pretype_float self f =
-    fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
-      let resj =
-        try Typing.judge_of_float !!env f
-        with Invalid_argument _ ->
-          user_err ?loc ~hdr:"pretype" (str "Type of float should be registered first.")
-        in
-        discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
-
 (* [pretype_type valcon env sigma c] coerces [c] into a type *)
 let pretype_type self c ?loc ~program_mode ~poly resolve_tc valcon (env : GlobEnv.t) sigma = match DAst.get c with
   | GHole (knd, naming, None) ->
@@ -1255,6 +1240,52 @@ let pretype_type self c ?loc ~program_mode ~poly resolve_tc valcon (env : GlobEn
                 ?loc:(loc_of_glob_constr c) !!env sigma tj.utj_val v
           end
 
+  let pretype_int self i =
+    fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
+        let resj =
+          try Typing.judge_of_int !!env i
+          with Invalid_argument _ ->
+            user_err ?loc ~hdr:"pretype" (str "Type of int63 should be registered first.")
+        in
+        discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
+
+  let pretype_float self f =
+    fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
+      let resj =
+        try Typing.judge_of_float !!env f
+        with Invalid_argument _ ->
+          user_err ?loc ~hdr:"pretype" (str "Type of float should be registered first.")
+        in
+        discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
+
+  let pretype_array self (u,t,def,ty) =
+    fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
+    let sigma, tycon' = split_as_array !!env sigma tycon in
+    let sigma, jty = eval_type_pretyper self ~program_mode ~poly resolve_tc tycon' env sigma ty in
+    (* XXX not sure if we need to be this complex, I wrote this while
+       being confused by broken universe substitutions *)
+    let sigma, u = match Univ.Universe.level (Sorts.univ_of_sort jty.utj_type) with
+      | Some u ->
+        let sigma = Evd.make_nonalgebraic_variable sigma u in
+        sigma, u
+      | None ->
+        let sigma, u = Evd.new_univ_level_variable UState.univ_flexible sigma in
+        let sigma = Evd.set_leq_sort !!env sigma jty.utj_type
+            (Sorts.sort_of_univ (Univ.Universe.make u))
+        in
+        sigma, u
+    in
+    let sigma, jdef = eval_pretyper self ~program_mode ~poly resolve_tc (mk_tycon jty.utj_val) env sigma def in
+    let pretype_elem = eval_pretyper self ~program_mode ~poly resolve_tc (mk_tycon jty.utj_val) env in
+    let sigma, jt = Array.fold_left_map pretype_elem sigma t in
+    let u = Univ.Instance.of_array [| u |] in
+    let ta = EConstr.of_constr @@ Typeops.type_of_array !!env u in
+    let j = {
+      uj_val = EConstr.mkArray(EInstance.make u, Array.map (fun j -> j.uj_val) jt, jdef.uj_val, jty.utj_val);
+      uj_type = EConstr.mkApp(ta,[|jdef.uj_type|])
+    } in
+    discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon
+
 end
 
 (* [pretype tycon env sigma lvar lmeta cstr] attempts to type [cstr] *)
@@ -1281,6 +1312,7 @@ let default_pretyper =
     pretype_cast = pretype_cast;
     pretype_int = pretype_int;
     pretype_float = pretype_float;
+    pretype_array = pretype_array;
     pretype_type = pretype_type;
   }
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 8be7b1477b..c03374c59f 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -163,6 +163,7 @@ type pretyper = {
   pretype_cast : pretyper -> glob_constr * glob_constr cast_type -> unsafe_judgment pretype_fun;
   pretype_int : pretyper -> Uint63.t -> unsafe_judgment pretype_fun;
   pretype_float : pretyper -> Float64.t -> unsafe_judgment pretype_fun;
+  pretype_array : pretyper -> glob_level list option * glob_constr array * glob_constr * glob_constr -> unsafe_judgment pretype_fun;
   pretype_type : pretyper -> glob_constr -> unsafe_type_judgment pretype_fun;
 }
 (** Type of pretyping algorithms in open-recursion style. A typical way to
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 18a0637efa..6f02d76f3a 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -422,8 +422,8 @@ struct
   let get_next_primitive_args kargs stk =
     let rec nargs = function
       | [] -> 0
-      | CPrimitives.Kwhnf :: _ -> 0
-      | _ :: s -> 1 + nargs s
+      | (CPrimitives.Kwhnf | CPrimitives.Karg) :: _ -> 0
+      | CPrimitives.Kparam :: s -> 1 + nargs s
     in
     let n = nargs kargs in
     (List.skipn (n+1) kargs, strip_n_app n stk)
@@ -588,6 +588,7 @@ struct
   type elem = EConstr.t
   type args = EConstr.t array
   type evd = evar_map
+  type uinstance = EConstr.EInstance.t
 
   let get = Array.get
 
@@ -601,6 +602,11 @@ struct
     | Float f -> f
     | _ -> raise Primred.NativeDestKO
 
+  let get_parray evd e =
+    match EConstr.kind evd e with
+    | Array(_u,t,def,_ty) -> Parray.of_array t def
+    | _ -> raise Not_found
+
   let mkInt env i =
     mkInt i
 
@@ -611,12 +617,12 @@ struct
     let (ct,cf) = get_bool_constructors env in
     mkConstruct (if b then ct else cf)
 
-    let mkCarry env b e =
-      let int_ty = mkConst @@ get_int_type env in
-      let (c0,c1) = get_carry_constructors env in
-      mkApp (mkConstruct (if b then c1 else c0),[|int_ty;e|])
+  let mkCarry env b e =
+    let int_ty = mkConst @@ get_int_type env in
+    let (c0,c1) = get_carry_constructors env in
+    mkApp (mkConstruct (if b then c1 else c0),[|int_ty;e|])
 
-    let mkIntPair env e1 e2 =
+  let mkIntPair env e1 e2 =
     let int_ty = mkConst @@ get_int_type env in
     let c = get_pair_constructor env in
     mkApp(mkConstruct c, [|int_ty;int_ty;e1;e2|])
@@ -699,6 +705,11 @@ struct
     let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,nan) =
       get_f_class_constructors env in
     mkConstruct nan
+
+  let mkArray env u t ty =
+    let (t,def) = Parray.to_array t in
+    mkArray(u,t,def,ty)
+
 end
 
 module CredNative = RedNative(CNativeEntries)
@@ -767,7 +778,7 @@ let rec whd_state_gen flags env sigma =
           let body = EConstr.of_constr body in
           whrec (body, stack)
           end
-       | exception NotEvaluableConst (IsPrimitive p) when Stack.check_native_args p stack ->
+       | exception NotEvaluableConst (IsPrimitive (u,p)) when Stack.check_native_args p stack ->
           let kargs = CPrimitives.kind p in
           let (kargs,o) = Stack.get_next_primitive_args kargs stack in
           (* Should not fail thanks to [check_native_args] *)
@@ -841,9 +852,9 @@ let rec whd_state_gen flags env sigma =
         |_ -> fold ()
       else fold ()
 
-    | Int _ | Float _ ->
+    | Int _ | Float _ | Array _ ->
       begin match Stack.strip_app stack with
-       | (_, Stack.Primitive(p,kn,rargs,kargs)::s) ->
+       | (_, Stack.Primitive(p,(_, u as kn),rargs,kargs)::s) ->
          let more_to_reduce = List.exists (fun k -> CPrimitives.Kwhnf = k) kargs in
          if more_to_reduce then
            let (kargs,o) = Stack.get_next_primitive_args kargs s in
@@ -858,10 +869,11 @@ let rec whd_state_gen flags env sigma =
              with List.IndexOutOfRange -> (args,[]) (* FIXME probably useless *)
            in
            let args = Array.of_list (Option.get (Stack.list_of_app_stack (rargs @ Stack.append_app [|x|] args))) in
-             begin match CredNative.red_prim env sigma p args with
-               | Some t -> whrec (t,s)
-               | None -> ((mkApp (mkConstU kn, args), s))
-             end
+           let s = extra_args @ s in
+           begin match CredNative.red_prim env sigma p u args with
+             | Some t -> whrec (t,s)
+             | None -> ((mkApp (mkConstU kn, args), s))
+           end
        | _ -> fold ()
       end
 
@@ -942,7 +954,7 @@ let local_whd_state_gen flags _env sigma =
       else s
 
     | Rel _ | Var _ | Sort _ | Prod _ | LetIn _ | Const _  | Ind _ | Proj _
-      | Int _ | Float _ -> s
+      | Int _ | Float _ | Array _ -> s
 
   in
   whrec
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 58fff49faa..b316b3c213 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -23,6 +23,7 @@ val debug_RAKAM : unit -> bool
 
 module CredNative : Primred.RedNative with
   type elem = EConstr.t and type args = EConstr.t array and type evd = Evd.evar_map
+  and type uinstance = EInstance.t
 
 (** Machinery to customize the behavior of the reduction *)
 module ReductionBehaviour : sig
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index bb518bc2f9..ebf9d4ed1c 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -157,6 +157,9 @@ let retype ?(polyprop=true) sigma =
     | Sort _ | Prod _ -> mkSort (sort_of env cstr)
     | Int _ -> EConstr.of_constr (Typeops.type_of_int env)
     | Float _ -> EConstr.of_constr (Typeops.type_of_float env)
+    | Array(u, _, _, ty) ->
+      let arr = EConstr.of_constr @@ Typeops.type_of_array env (EInstance.kind sigma u) in
+      mkApp(arr, [|ty|])
 
   and sort_of env t =
     match EConstr.kind sigma t with
@@ -301,8 +304,7 @@ let relevance_of_term env sigma c =
       | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance
       | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance
       | Proj (p, _) -> Relevanceops.relevance_of_projection env p
-      | Int _ | Float _ -> Sorts.Relevant
-
+      | Int _ | Float _ | Array _ -> Sorts.Relevant
       | Meta _ | Evar _ -> Sorts.Relevant
 
     in
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index b4a1153731..756ccd3438 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -332,6 +332,23 @@ let judge_of_int env v =
 let judge_of_float env v =
   Environ.on_judgment EConstr.of_constr (judge_of_float env v)
 
+let judge_of_array env sigma u tj defj tyj =
+  let ulev = match Univ.Instance.to_array u with
+    | [|u|] -> u
+    | _ -> assert false
+  in
+  let sigma = Evd.set_leq_sort env sigma tyj.utj_type
+      (Sorts.sort_of_univ (Univ.Universe.make ulev))
+  in
+  let check_one sigma j = Evarconv.unify_leq_delay env sigma j.uj_type tyj.utj_val in
+  let sigma = check_one sigma defj in
+  let sigma = Array.fold_left check_one sigma tj in
+  let arr = EConstr.of_constr @@ type_of_array env u in
+  let j = make_judge (mkArray(EInstance.make u, Array.map j_val tj, defj.uj_val, tyj.utj_val))
+      (mkApp (arr, [|tyj.utj_val|]))
+  in
+  sigma, j
+
 (* cstr must be in n.f. w.r.t. evars and execute returns a judgement
    where both the term and type are in n.f. *)
 let rec execute env sigma cstr =
@@ -455,6 +472,13 @@ let rec execute env sigma cstr =
     | Float f ->
         sigma, judge_of_float env f
 
+    | Array(u,t,def,ty) ->
+      let sigma, tyj = execute env sigma ty in
+      let sigma, tyj = type_judgment env sigma tyj in
+      let sigma, defj = execute env sigma def in
+      let sigma, tj = execute_array env sigma t in
+      judge_of_array env sigma (EInstance.kind sigma u) tj defj tyj
+
 and execute_recdef env sigma (names,lar,vdef) =
   let sigma, larj = execute_array env sigma lar in
   let sigma, lara = Array.fold_left_map (assumption_of_judgment env) sigma larj in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ef58f41489..a26c981cb9 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -564,7 +564,7 @@ let is_rigid_head sigma flags t =
   match EConstr.kind sigma t with
   | Const (cst,u) -> not (TransparentState.is_transparent_constant flags.modulo_delta cst)
   | Ind (i,u) -> true
-  | Construct _ | Int _ | Float _ -> true
+  | Construct _ | Int _ | Float _ | Array _ -> true
   | Fix _ | CoFix _ -> true
   | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod _
     | Lambda _ | LetIn _ | App (_, _) | Case (_, _, _, _, _)
@@ -659,7 +659,7 @@ let rec is_neutral env sigma ts t =
     | Evar _ | Meta _ -> true
     | Case (_, p, _, c, _) -> is_neutral env sigma ts c
     | Proj (p, c) -> is_neutral env sigma ts c
-    | Lambda _ | LetIn _ | Construct _ | CoFix _ | Int _ | Float _ -> false
+    | Lambda _ | LetIn _ | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> false
     | Sort _ | Cast (_, _, _) | Prod (_, _, _) | Ind _ -> false (* Really? *)
     | Fix _ -> false (* This is an approximation *)
     | App _ -> assert false
@@ -1819,6 +1819,15 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
                with ex when precatchable_exception ex ->
                  matchrec c)
 
+          | Array(_u,t,def,ty) ->
+            (try
+              matchrec def
+            with ex when precatchable_exception ex ->
+             try
+              matchrec ty
+            with ex when precatchable_exception ex ->
+              iter_fail matchrec t)
+
           | Cast (_, _, _) (* Is this expected? *)
           | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Const _ | Ind _
             | Construct _ | Int _ | Float _ -> user_err Pp.(str "Match_subterm")))
@@ -1887,6 +1896,9 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
             | Lambda (_,t,c) ->
                 bind (matchrec t) (matchrec c)
 
+            | Array(_u,t,def,ty) ->
+              bind (bind (bind_iter matchrec t) (matchrec def)) (matchrec ty)
+
           | Cast (_, _, _)  -> fail "Match_subterm" (* Is this expected? *)
 
           | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Const _ | Ind _
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index efe1efd74e..b3f577b684 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -170,6 +170,7 @@ and nf_whd env sigma whd typ =
       mkApp(capp,args)
   | Vint64 i -> i |> Uint63.of_int64 |> mkInt
   | Vfloat64 f -> f |> Float64.of_float |> mkFloat
+  | Varray t -> nf_array env sigma t typ
   | Vatom_stk(Aid idkey, stk) ->
       constr_type_of_idkey env sigma idkey stk
   | Vatom_stk(Aind ((mi,i) as ind), stk) ->
@@ -399,6 +400,14 @@ and nf_cofix env sigma cf =
   let cfb = Util.Array.map2 (fun v t -> nf_val env sigma v t) vb cft in
   mkCoFix (init,(names,cft,cfb))
 
+and nf_array env sigma t typ =
+  let ty, allargs = decompose_appvect (whd_all env typ) in
+  let typ_elem = allargs.(0) in
+  let t, vdef = Parray.to_array t in
+  let t = Array.map (fun v -> nf_val env sigma v typ_elem) t in
+  let u = snd (destConst ty) in
+  mkArray(u, t, nf_val env sigma vdef typ_elem, typ_elem)
+
 let cbv_vm env sigma c t  =
   if Termops.occur_meta sigma c then
     CErrors.user_err Pp.(str "vm_compute does not support metas.");