Disable new warnings for Coq master

Disable some warnings for Coq master. Fixing the underlying issue in the code would be incompatible with previous versions of Coq: Declare Scope is a new command, and the change_no_check tactic that replaces convert_concl_no_check is also new.