Open mattam82 opened 4 months ago
Adapt to Coq's new support for algebraic universes everywhere. Also fix the derivation of noconf/noconfhom which introduced unnecessary universes.
Adapt to Coq's new support for algebraic universes everywhere. Also fix the derivation of noconf/noconfhom which introduced unnecessary universes.