Follows Rec!3217
Rename MIN_E
and MAX_E
functors into MIN_ELEMENT
and MAX_ELEMENT
Needs Rec!3217 (merged), Analysis!932 (merged), DaVinci!795 (merged)
Edited by Tommaso Fulghesu
Rename MIN_E
and MAX_E
functors into MIN_ELEMENT
and MAX_ELEMENT
Needs Rec!3217 (merged), Analysis!932 (merged), DaVinci!795 (merged)