Use Compat.Coq816 instead of Compat.Coq814

For coq/coq#16821
JasonGross · Nov 17, 2022 · 153ac32 · 153ac32
1 parent 3711598
commit 153ac32
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 4 deletions.
diff --git a/compatibility/Coq__8_16__Compat.v b/compatibility/Coq__8_16__Compat.v
@@ -3,7 +3,7 @@
 (** Compatibility file for making Coq act similar to Coq v8.8 *)
 Local Set Warnings "-deprecated".
 
-Require Export Coq.Compat.Coq814.
+Require Export Coq.Compat.Coq816.
 
 Unset Private Polymorphic Universes.
 
@@ -27,6 +27,7 @@ Number Notation Int31.int31 Int31.phi_inv_nonneg Int31.phi : int31_scope.
 Local Set Warnings "-deprecated".
 Global Set Firstorder Solver auto with *.
 Global Set Instance Generalized Output.
+Global Set Apply With Renaming.
 
 Require Coq.micromega.Lia.
 Module Export Coq.

diff --git a/compatibility/Coq__8_17__Compat.v b/compatibility/Coq__8_17__Compat.v
@@ -3,7 +3,7 @@
 (** Compatibility file for making Coq act similar to Coq v8.8 *)
 Local Set Warnings "-deprecated".
 
-Require Export Coq.Compat.Coq814.
+Require Export Coq.Compat.Coq816.
 
 Unset Private Polymorphic Universes.
 
@@ -27,6 +27,7 @@ Number Notation Int31.int31 Int31.phi_inv_nonneg Int31.phi : int31_scope.
 Local Set Warnings "-deprecated".
 Global Set Firstorder Solver auto with *.
 Global Set Instance Generalized Output.
+Global Set Apply With Renaming.
 
 Require Coq.micromega.Lia.
 Module Export Coq.

diff --git a/compatibility/Coq__master__Compat.v b/compatibility/Coq__master__Compat.v
@@ -3,7 +3,7 @@
 (** Compatibility file for making Coq act similar to Coq v8.8 *)
 Local Set Warnings "-deprecated".
 
-Require Export Coq.Compat.Coq814.
+Require Export Coq.Compat.Coq816.
 
 Unset Private Polymorphic Universes.
 
@@ -27,6 +27,7 @@ Number Notation Int31.int31 Int31.phi_inv_nonneg Int31.phi : int31_scope.
 Local Set Warnings "-deprecated".
 Global Set Firstorder Solver auto with *.
 Global Set Instance Generalized Output.
+Global Set Apply With Renaming.
 
 Require Coq.micromega.Lia.
 Module Export Coq.

diff --git a/compatibility/fragments/Grab88v816.v b/compatibility/fragments/Grab88v816.v
@@ -1,7 +1,7 @@
 (** Compatibility file for making Coq act similar to Coq v8.8 *)
 Local Set Warnings "-deprecated".
 
-Require Export Coq.Compat.Coq814.
+Require Export Coq.Compat.Coq816.
 
 Unset Private Polymorphic Universes.
 
@@ -25,6 +25,7 @@ Number Notation Int31.int31 Int31.phi_inv_nonneg Int31.phi : int31_scope.
 Local Set Warnings "-deprecated".
 Global Set Firstorder Solver auto with *.
 Global Set Instance Generalized Output.
+Global Set Apply With Renaming.
 
 Require Coq.micromega.Lia.
 Module Export Coq.