Use : Set explicitly when needed

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps

MIT License

42 stars 24 forks source link

Closed SkySkimmer closed 1 year ago

SkySkimmer commented 1 year ago

More robust given use of Unset Universe Minimization ToSet, cf https://github.com/coq/coq/pull/17810 and related

SkySkimmer commented 1 year ago

Please merge