mathlib3
d33341c9 - Remove local_names_option

Commit
5 years ago
Remove local_names_option
Author
Parents
Loading