Adapt wrt Coq/Coq#18164

MetaCoq / metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq

https://metacoq.github.io

MIT License

368 stars 79 forks source link

Closed Villetaneuse closed 10 months ago

Villetaneuse commented 10 months ago

The error is:

 File "./theories/TemplateMonadToPCUIC.v", line 185, characters 20-49:
  Error: Error: Universe instance length is 2 but should be 3.

So, what happened here? @mattam82 @tabareau

It did build locally against my coq dev branch (did not try to build it against coq-dev or other versions of coq, because it takes a lot of time).

ppedrot commented 10 months ago

Does MetaCoq compile on master?