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 sure`MCList`

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