diff options
| author | Gaëtan Gilbert | 2018-11-06 15:20:35 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-22 13:33:22 +0100 |
| commit | 47e192dfa40de25a1d1cc51cbd5c6191cdea21b3 (patch) | |
| tree | c047f7e57bd278a9f05486d88dbf1921f198570f | |
| parent | a7cf802627a9842862c6290496d73a815ab2f42b (diff) | |
Disable deprecation warnings in compat files.
| -rw-r--r-- | theories/Compat/Coq87.v | 2 | ||||
| -rw-r--r-- | theories/Compat/Coq88.v | 2 | ||||
| -rw-r--r-- | theories/Compat/Coq89.v | 1 |
3 files changed, 5 insertions, 0 deletions
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". |