1 files changed, 11 insertions, 1 deletions
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) ()