Stream: MetaCoq

Topic: Build errors (coq#17022)

view this post on Zulip 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)

view this post on Zulip Gaëtan Gilbert (Feb 08 2023 at 15:50):

you need to rebase your coq branch to get https://github.com/coq/coq/pull/17194

Last updated: Apr 19 2024 at 12:02 UTC