Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Mathcomp master integration ereal #189

Closed

Conversation

affeldt-aist
Copy link
Member

work in progress, supersedes PR #137

@affeldt-aist affeldt-aist marked this pull request as draft April 24, 2020 21:42
@affeldt-aist affeldt-aist mentioned this pull request Apr 24, 2020
@affeldt-aist affeldt-aist force-pushed the mathcomp_master_integration_ereal branch 4 times, most recently from e090367 to 7015491 Compare April 26, 2020 23:57
@CohenCyril
Copy link
Member

should be reopened on top of master

@affeldt-aist affeldt-aist force-pushed the mathcomp_master_hausdorff_close branch from 5fcd283 to 4f1de13 Compare April 29, 2020 16:16
@affeldt-aist affeldt-aist force-pushed the mathcomp_master_integration_ereal branch 4 times, most recently from f7e47a4 to 1b0b76a Compare April 29, 2020 17:44
@CohenCyril CohenCyril force-pushed the mathcomp_master_hausdorff_close branch from 4f1de13 to 17086dc Compare May 4, 2020 15:31
@CohenCyril CohenCyril force-pushed the mathcomp_master_integration_ereal branch from 1b0b76a to e1b8280 Compare May 4, 2020 15:42
@CohenCyril CohenCyril force-pushed the mathcomp_master_hausdorff_close branch from 17086dc to 7d1689b Compare May 6, 2020 18:26
@affeldt-aist affeldt-aist force-pushed the mathcomp_master_integration_ereal branch from ac94145 to 348f2a9 Compare May 14, 2020 14:04
@affeldt-aist affeldt-aist changed the base branch from mathcomp_master_hausdorff_close to master May 14, 2020 14:04
@affeldt-aist affeldt-aist force-pushed the mathcomp_master_integration_ereal branch 3 times, most recently from 22ba6a0 to 15ba457 Compare May 24, 2020 22:09
@affeldt-aist affeldt-aist force-pushed the mathcomp_master_integration_ereal branch from 15ba457 to 0d659c0 Compare June 1, 2020 20:58
@affeldt-aist affeldt-aist changed the base branch from master to ereal_pseudometric June 1, 2020 20:59
@affeldt-aist affeldt-aist force-pushed the mathcomp_master_integration_ereal branch from 0d659c0 to 412b8da Compare June 2, 2020 08:35
@affeldt-aist affeldt-aist force-pushed the mathcomp_master_integration_ereal branch from 412b8da to bbcff2e Compare June 3, 2020 11:07
theories/integral.v Outdated Show resolved Hide resolved
theories/integral.v Outdated Show resolved Hide resolved
@affeldt-aist affeldt-aist force-pushed the ereal_pseudometric branch 2 times, most recently from ae0f332 to ff2de7d Compare June 8, 2020 23:52
affeldt-aist and others added 2 commits June 9, 2020 09:50
Co-authored-by: Cyril Cohen <cohen@crans.org>
@affeldt-aist affeldt-aist force-pushed the mathcomp_master_integration_ereal branch from f57cbf5 to 8de8cb7 Compare June 9, 2020 01:01
@affeldt-aist
Copy link
Member Author

Is it ok to close this PR? Contents have been moved to PR #223 and PR #224 .

@CohenCyril
Copy link
Member

The diff confirms it is indeed subsumed!

@CohenCyril CohenCyril closed this Jun 10, 2020
@CohenCyril CohenCyril deleted the mathcomp_master_integration_ereal branch June 10, 2020 14:12
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