So it seems there are
coq-elpi issues again on
# CAMLC -c src/coq_elpi_utils.mli # CAMLC -c src/coq_elpi_HOAS.mli # File "src/coq_elpi_HOAS.mli", line 100, characters 62-86: # Error: Unbound module ComInductive.Mind_decl # make: *** [Makefile.coq:725: src/coq_elpi_HOAS.cmi] Error 2 # make: *** [Makefile:50: build-core] Error 2 # make: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-elpi.dev' # make: *** [Makefile:42: all] Error 2
See for example this build. Is this known, or can one do something?
hmm, I'm confused about the OCaml version here... could that be the issue? the
mathcomp-dev:coq-dev Docker image is not up to date, and some old Coq
master is used?
Last updated: Feb 05 2023 at 13:02 UTC