search

MetaCoq / metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq
https://metacoq.github.io
MIT License
380 stars 82 forks source link

Use : Set explicitly when needed #971

Closed SkySkimmer closed 1 year ago

SkySkimmer commented 1 year ago

more robust when using Unset Universe Minimization ToSet cf https://github.com/coq/coq/pull/17810 https://github.com/coq/coq/pull/17795