MetaCoq / metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq
https://metacoq.github.io
MIT License
370 stars 79 forks source link

coq-8.17 branch no longer builds on ocaml 4.11.2 #1022

Open JasonGross opened 9 months ago

JasonGross commented 9 months ago
CAMLOPT -c -for-pack Template_coq src/quoter.ml
File "src/quoter.ml", line 345, characters 24-43:
345 |         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
                              ^^^^^^^^^^^^^^^^^^^
Error: Unbound value Array.fold_left_map
Command exited with non-zero status 2
src/quoter.cmx (real: 0.07, user: 0.06, sys: 0.00, mem: 26688 ko)
make[2]: *** [Makefile.template:743: src/quoter.cmx] Error 2
CAMLOPT -c -for-pack Template_coq src/denoter.ml
File "src/denoter.ml", line 166, characters 25-44:
166 |           let evm, arr = Array.fold_left_map (fun evm a -> aux env evm a) evm arr in
                               ^^^^^^^^^^^^^^^^^^^
Error: Unbound value Array.fold_left_map
Command exited with non-zero status 2
src/denoter.cmx (real: 0.06, user: 0.03, sys: 0.02, mem: 24656 ko)
make[2]: *** [Makefile.template:743: src/denoter.cmx] Error 2

Presumably this is due to https://github.com/MetaCoq/metacoq/pull/998 cc @mattam82 Is there an easy way to restore compatibility so I don't have to recompile my whole 8.17 switch?