Restore compatibility with OCaml < 4.13

Fixes MetaCoq#1022 after MetaCoq#998

template-coq/src/denoter.ml

@@ -163,7 +163,7 @@ struct
       | ACoq_tFloat x -> evm, Constr.mkFloat (D.unquote_float64 x)
       | ACoq_tArray (u, arr, def, ty) ->
           let evm, u = D.unquote_universe_level evm u in
-          let evm, arr = Array.fold_left_map (fun evm a -> aux env evm a) evm arr in
+          let evm, arr = ArrayCompat.fold_left_map (fun evm a -> aux env evm a) evm arr in
           let evm, def = aux env evm def in
           let evm, ty = aux env evm ty in
           evm, Constr.mkArray (Univ.Instance.of_array [|u|], arr, def, ty)

template-coq/src/quoter.ml

@@ -342,7 +342,7 @@ struct
         let u = match Univ.Instance.to_array u with [| u |] -> u | _ -> assert false in
         let def', acc = quote_term acc env sigma def in
         let ty', acc = quote_term acc env sigma ty in
-        let acc, arr' = Array.fold_left_map (fun acc t -> let t', acc = quote_term acc env sigma t in acc, t') acc ar in
+        let acc, arr' = ArrayCompat.fold_left_map (fun acc t -> let t', acc = quote_term acc env sigma t in acc, t') acc ar in
         Q.mkArray (Q.quote_univ_level u) arr' ~default:def' ~ty:ty', acc
       in
       aux acc env trm

template-coq/src/tm_util.ml

@@ -314,3 +314,20 @@ type ('term, 'nat, 'ident, 'name, 'quoted_sort, 'cast_kind, 'kername, 'inductive
   | ACoq_tFloat of 'float64
   | ACoq_tArray of 'universe_level * 'term array * 'term * 'term
 
+module ArrayCompat = struct
+  (** For compat with OCaml < 4.13, copied from https://github.com/ocaml/ocaml/blob/d5b5c34971ed4291c385852f820554ad57adba84/stdlib/array.ml#L195-L207 *)
+  let fold_left_map f acc input_array =
+    let open Array in
+    let len = length input_array in
+    if len = 0 then (acc, [||]) else begin
+      let acc, elt = f acc (unsafe_get input_array 0) in
+      let output_array = make len elt in
+      let acc = ref acc in
+      for i = 1 to len - 1 do
+        let acc', elt = f !acc (unsafe_get input_array i) in
+        acc := acc';
+        unsafe_set output_array i elt;
+      done;
+      !acc, output_array
+    end
+end