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.

Sign up for GitHub

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

Jump to bottom

adde_def or adde_undef #365

Closed
affeldt-aist opened this issue Apr 1, 2021 · 0 comments · Fixed by #394
Closed

adde_def or adde_undef #365

affeldt-aist opened this issue Apr 1, 2021 · 0 comments · Fixed by #394
Milestone
0.3.10

Comments

@affeldt-aist
Copy link
Member

analysis/theories/ereal.v

Line 405 in 4098cb9

Definition adde_undef x y :=

maybe adde_def if we use too many ~~ adde_undef
@affeldt-aist affeldt-aist added this to the 0.3.8 milestone Apr 1, 2021
@CohenCyril CohenCyril mentioned this issue May 4, 2021
Merged
@affeldt-aist affeldt-aist modified the milestones: 0.3.8, 0.3.9 May 29, 2021
@affeldt-aist affeldt-aist modified the milestones: 0.3.9, 0.3.10 Jun 14, 2021
affeldt-aist added a commit that referenced this issue Jun 17, 2021
@affeldt-aist
fixes #365
a4e309d
@affeldt-aist affeldt-aist mentioned this issue Jun 17, 2021
Merged
affeldt-aist added a commit that referenced this issue Jun 22, 2021
@affeldt-aist
Merge pull request #394 from math-comp/fixes_365
b46f824 
fixes #365
thery pushed a commit to thery/analysis that referenced this issue Jan 29, 2022
@affeldt-aist @thery
fixes math-comp#365
9f16e44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
0.3.10
Development

Successfully merging a pull request may close this issue.

fixes #365 math-comp/analysis
1 participant
@affeldt-aist