Christian Doczkal

To make this progress, there are several questions that need to be answered: 1. Does the technical setup meet the mathcomp standards or what would need to be adapted 2....

> I think most classes should be translated to canonical structures (except for Setoid equality that you depend on for rewrite and code sharing). What is the technical benefit of...

If I create a pull-request, should I add this as a module at the end of `bigop.v` or where should this go?

For the record: Daniel Kirk voiced interest in this on [Zulip](https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/Bigop.20and.20the.20direct.20sum.20of.20modules). Maybe we can make some progress?

@gares. Yes, you got the right package and for me it is still failing as of 5 minutes ago: https://github.com/coq-community/graph-theory/runs/1531187774

Great! Thanks for the info! So the the world of `coq-native` now makes peoples "pure .v" developments sensitive to the underlying Version of OCaml. IIRC, this is precisely the thing...

Given that the error you managed to reproduce comes from our library, feel free to contact me if you think I can help. Admittedly, this is a somewhat ad-hoc corner...

I recently stumbled across this tool and I would like to second this feature request, in particular the whitelisting by keywords (i.e., `Theorem` as well as `Proposition`, `Fact`, and `Example`)....

It seems this issue has been dormant for a while. However, together with #63 it is what's currently keeping me from using `dpdraph` for my graph theory project. This project...

What about an option take a diff (e.g., the current local changes) and open the GitHub website with an in-progress review where the diffs have been turned into suggestions, so...