There are two branches about Hahn-Banach on the github of MCA that are quite old (5-6 years):
https://github.com/math-comp/analysis/tree/mathcomp_master_hahnbanach
https://github.com/math-comp/analysis/tree/hahnbanach
Is it ok to remove them (now that Hahn-Banach has landed in master)? @mkerjean
There are two branches about Hahn-Banach on the github of MCA that are quite old (5-6 years):
https://github.com/math-comp/analysis/tree/mathcomp_master_hahnbanach
https://github.com/math-comp/analysis/tree/hahnbanach
Is it ok to remove them (now that Hahn-Banach has landed in master)? @mkerjean