Skip to content

Conversation

@zstone1
Copy link
Contributor

@zstone1 zstone1 commented Nov 18, 2024

Paths on bipointed spaces, and path chaining. More pieces of #1350

Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

@affeldt-aist
Copy link
Member

The documentation of wedge2p does not mention its b argument.
It is also out of order (bpwedge comes before wedge2p even though the latter is defined before for the former).
Isn't there a better name for wedge2p? (When p is a prefix, it is understood that it means "pointed", but here the 2p prefix might be confusing.) What about bpwedge_shared_pt?

@affeldt-aist
Copy link
Member

The CI fails in tvs.v:

       > File "./tvs.v", line 127, characters 10-32:
       > Error: Cannot apply lemma nbhs0N_subproof

It looks like an error with MathComp's master. Maybe @mkerjean has a clue.

@affeldt-aist affeldt-aist self-requested a review November 19, 2024 03:44
Copy link
Member

@affeldt-aist affeldt-aist left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should maybe make the CI green before merging.

@zstone1 zstone1 merged commit 71b1296 into math-comp:master Nov 21, 2024
31 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants