Skip to content
GitLab
Explore
Sign in
Rename `_plus` into `_add`.
Code
Review changes
Check out branch
Download
Patches
Plain diff
Robbert Krebbers
requested to merge
robbert/laterN_add
into
master
Jul 26, 2022
Overview
6
Commits
2
Pipelines
2
Changes
4
Expand
This fixes
#472 (closed)
.
See also
stdpp!404 (merged)
Edited
Aug 09, 2022
by
Robbert Krebbers
Merge request reports