no need to allow any warnings

_CoqProject

 -Q exercises exercises
 -Q solutions solutions
 -Q talks/demo demo
-# change_no_check does not exist yet in 8.9.
--arg -w -arg -convert_concl_no_check
-# We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
--arg -w -arg -ambiguous-paths
-# Can be triggered when importing some Iris files.
--arg -w -arg -notation-overridden
 
 talks/demo/part1.v
 talks/demo/part2.v