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 but I get a different build error when I run make -f 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/", 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

Last updated: Jun 04 2023 at 23:30 UTC