Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
JasonGross opened this issue Nov 30, 2023 · 0 comments
Open

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

JasonGross opened this issue Nov 30, 2023 · 0 comments

Comments

@JasonGross
Copy link
Contributor

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 #998 cc @mattam82
Is there an easy way to restore compatibility so I don't have to recompile my whole 8.17 switch?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant