diff options
| -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". |