search

jwiegley / category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work
BSD 3-Clause "New" or "Revised" License
748 stars 69 forks source link

Adapt w.r.t. coq/coq#18910. #143

Closed ppedrot closed 5 months ago

ppedrot commented 6 months ago

We guide unification a bit to prevent TC resolution from relying on a previously transparent Coq primitive.

Should be backwards compatible.

ppedrot commented 5 months ago

Ping @jwiegley just in case. I'd like to go this in a soon as possible to be sure that the corresponding PR in Coq master goes into 8.20.

jwiegley commented 5 months ago

The merge button on GitHub is not working today. I will try merging this manually.

ppedrot commented 5 months ago

Thanks!