Skip to content

Disable new warnings for Coq master

Tej Chajed requested to merge tchajed/iris-coq:disable-warnings into 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.

Merge request reports