fix coq-makefile warnings and bring back Coq 8.16

.gitlab-ci.yml

@@ -33,7 +33,13 @@ build-coq.8.17.0:
   <<: *template
   variables:
     OPAM_PINS: "coq version 8.17.0"
-    #DENY_WARNINGS: "1" # coq_makefile warning cannot be resolved while supporting Coq 8.14
+    DENY_WARNINGS: "1" # coq_makefile warning cannot be resolved while supporting Coq 8.14
+
+build-coq.8.16.1:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.16.1"
+    DENY_WARNINGS: "1"
 
 trigger-iris.dev:
   <<: *template

README.md

@@ -13,7 +13,7 @@ This tutorial comes in two versions:
 
 For the tutorial material you need to have the following dependencies installed:
 
-- Coq 8.17.0
+- Coq 8.16.1 / 8.17.0
 - A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
 
 *Note:* the tutorial material will not work with earlier versions of Iris, it

_CoqProject

 -Q solutions solutions
 -Q exercises exercises
-INSTALLDEFAULTROOT = tutorial-popl20
+-docroot tutorial-popl20
 
 solutions/language.v
 solutions/polymorphism.v