Minutes September 22 2021 - math-comp/math-comp GitHub Wiki

A demo/explanation of the morphism support in Algebra Tactics

by Kazuhiko Sakaguchi

@ybertot : mostly satisfied with the new search [heavy user of Search]
- maybe need a bit more of testing, still migration work in progress
- I like I can filter easily using + and -
@cyrilcohen :
- need for better syntax, for example for module qualification
- new search should be good, modulo some syntax improvements
Sometimes it is hard to remember all the options, for example head_concl: vs concl: [pointed by several people] , a bit of a learning curve
generally people in the meeting has no complaints about the removal

Wait a bit more to provide definitive feedback from more users: open a thread on Zulip to consult more users: decision on 1 month