From 47e192dfa40de25a1d1cc51cbd5c6191cdea21b3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 6 Nov 2018 15:20:35 +0100
Subject: Disable deprecation warnings in compat files.

---
 theories/Compat/Coq87.v | 2 ++
 theories/Compat/Coq88.v | 2 ++
 theories/Compat/Coq89.v | 1 +
 3 files changed, 5 insertions(+)

diff --git a/theories/Compat/Coq87.v b/theories/Compat/Coq87.v
index dc1397aff2..5e031efa85 100644
--- a/theories/Compat/Coq87.v
+++ b/theories/Compat/Coq87.v
@@ -9,6 +9,8 @@
 (************************************************************************)
 
 (** Compatibility file for making Coq act similar to Coq v8.7 *)
+Local Set Warnings "-deprecated".
+
 Require Export Coq.Compat.Coq88.
 
 (* In 8.7, omega wasn't taking advantage of local abbreviations,
diff --git a/theories/Compat/Coq88.v b/theories/Compat/Coq88.v
index 0aab64e4c4..989072940a 100644
--- a/theories/Compat/Coq88.v
+++ b/theories/Compat/Coq88.v
@@ -9,6 +9,8 @@
 (************************************************************************)
 
 (** Compatibility file for making Coq act similar to Coq v8.8 *)
+Local Set Warnings "-deprecated".
+
 Require Export Coq.Compat.Coq89.
 
 (** In Coq 8.9, prim token notations follow [Import] rather than
diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v
index d25671887f..49b9e4c951 100644
--- a/theories/Compat/Coq89.v
+++ b/theories/Compat/Coq89.v
@@ -9,3 +9,4 @@
 (************************************************************************)
 
 (** Compatibility file for making Coq act similar to Coq v8.9 *)
+Local Set Warnings "-deprecated".
-- 
cgit v1.2.3