diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ada1ff7d4a0b59260658bac7cf076df56aeabf57..780f9ebcbe0e759b228ab856a98be950405f1833 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -47,6 +47,7 @@ build-coq.8.14.dev: OPAM_PINS: "coq version 8.14.dev" MANGLE_NAMES: "1" CI_COQCHK: "1" + DENY_WARNINGS: "1" build-coq.8.13.2: <<: *template diff --git a/_CoqProject b/_CoqProject index 77e45b94de9eec153fba2fe35d973172793159ac..6ea277df73f7bcd40ab35a6bc0b7514b9d4c6e32 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,4 +1,6 @@ -Q theories stdpp +# 'Global Hint Rewrite' not supported before Coq 8.14. +-arg -w -arg -deprecated-hint-rewrite-without-locality theories/options.v theories/base.v