diff --git a/_CoqProject b/_CoqProject index 78d8e4df4415a915769364a103b736336f9aa91c..d6dd2d82030bee165a2f94705f314db6172583af 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,6 +1,8 @@ -Q theories stdpp # 'Global Hint Rewrite' not supported before Coq 8.14. -arg -w -arg -deprecated-hint-rewrite-without-locality +# Fixing this one requires Coq 8.15. +-arg -w -arg -deprecated-typeclasses-transparency-without-locality theories/options.v theories/base.v