Drop support for Coq 8.9?

Should we drop support for Coq 8.9? Let us collect what we would get by requiring Coq 8.10.

• #317 requires 8.10 I think.
• non-canonical projections
• change_no_check (to stop using deprecated convert_concl_no_check)
• Declare Scope (to fix deprecated use of undeclared scopes)

Is there more?