Skip to content

Draft: Prepare MathComp pull request

Pierre Roux requested to merge prepare_MC_PR into master

This is in preparation of a pull request to MathComp to push generic lemmas upstream (I only went through util/nat.v anf util/sum.v for now). Merge plan:

  • do a pull request on MathComp with the lemmas tagged TODO: PR MathComp
  • when this PR is merged, adapt the current merge request and change the TODO comments into something like "will be in MathComp 1.15"
  • merge the current merge request
  • once MathComp 1.15 (or 2.0) is released and becomes the minimal version in Prosa, remove the tagged lemmas

Is there a volunteer to open the upstream pull request? I could certainly do it but I don't feel the most legitimate, not being an actual Prosa author. Note that I probably already made most of the work here by rewriting the proofs in a more MathComp style, so the procces should be reasonnably light. It's also a great opportunity to learn more about MathComp and how to write short and robust proof scripts with ssreflect.

Edited by Pierre Roux

Merge request reports