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.
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.