Andres Erbsen (Feb 08 2023 at 15:49): Andres Erbsen (Feb 08 2023 at 15:49):Hi! I am trying to port metacoq over https://github.com/coq/coq/pull/17022/files but I get a different build error when I run make -f Makefile.ci ci-metacoq in my local Coq git work directory. Would anyone be willing to help me out here; either with this error or by making sureMCList builds after Require Btauto. Thanks! The error is below:
File "src/equations_common.ml", line 359, characters 32-46:
359 | let is_lglobal env sigma gr c = EConstr.isRefX env sigma (Lazy.force gr) c
^^^^^^^^^^^^^^
Error: This function has type
Evd.evar_map -> Names.GlobRef.t -> EConstr.t -> bool
It is applied to too many arguments; maybe you forgot a `;'.
Command exited with non-zero status 2
src/equations_common.cmx (real: 0.06, user: 0.05, sys: 0.01, mem: 32696 ko)
you need to rebase your coq branch to get https://github.com/coq/coq/pull/17194
Last updated: Jun 04 2023 at 23:30 UTC