Universe inconsistency with MetaCoq and stdpp

[4ever2]

The following code gives an error with MetaCoq 1.3.1+8.17 and coq-stdpp 1.9.0

From stdpp Require gmap.
From MetaCoq.Erasure Require EWcbvEval.

This gives the error:

Universe inconsistency. Cannot enforce Basics.flip.u0 =
Coq.MSets.MSetInterface.3 because Coq.MSets.MSetInterface.3
<= Coq.Lists.List.321 <= base.MRet.u0 <= fin_maps.MapFold.u2
< Basics.flip.u0.

This behavior was introduced in #1007 and might be related to the change here https://github.com/MetaCoq/metacoq/blame/67097a400c5889c03fd1f3f232b75d5391031a25/pcuic/theories/PCUICConfluence.v#L1426

[spitters]

@yannl35133 made that PR, so he may have some insights here...

[4ever2]

This fa4b728 commit fixes the issue. Thanks for the help.
I see that the commit was not included in the 1.3.2 release. This issue is blocking upgrading a few of our projects, so any chance that it can be included in the next release?

[mattam82]

Sorry for missing this, the fix is now in all the branches and will be part of the next release.

[spitters]

Thanks @mattam82 for the prompt response!