Skip to content
GitLab

Silence uninteresting Coq warnings, including the useless 8.10 ones

Merged Paolo G. Giarrusso requested to merge Blaisorblade/tutorial-popl18:hide-warnings into master

Tested with Iris dev.2019-11-02.2.ea809ed4 (everything else works).