Closed jjhugues closed 2 weeks ago
@jwiegley would you welcome a PR on this or is there anything you want to check first?
If this passes our CI, I'd happily accept such a PR, thank you.
@jjhugues Would you be willing to submit that PR? Happy to merge it.
Sorry it sat on my repo for so long.
No worries! I'm grateful for the work, whenever it gets in. :)
Lib/Foundation.v
defines notations for ∀ , ∃, and λIf user code imports both
Category.Lib
andUtf8
from the Coq standard library, we get the following error messageThe following patch seems enough to work around this issue: I confirmed
category-theory
compiles and so does my code. Before proposing a pull request, I am curious about your feedback on this. I must admit my patch is pretty arbitrary, it ressembles the notation definition from the Coq standard library to avoid conflicts.Thanks,