diff --git a/template-coq/src/denoter.ml b/template-coq/src/denoter.ml index 880033ac2..5a0030681 100644 --- a/template-coq/src/denoter.ml +++ b/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) diff --git a/template-coq/src/quoter.ml b/template-coq/src/quoter.ml index 9dbd3018a..2eadb282c 100644 --- a/template-coq/src/quoter.ml +++ b/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 diff --git a/template-coq/src/tm_util.ml b/template-coq/src/tm_util.ml index 50ec20253..47ee0da67 100644 --- a/template-coq/src/tm_util.ml +++ b/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