diff options
| author | Gaëtan Gilbert | 2020-11-02 15:16:32 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-15 10:30:31 +0100 |
| commit | f8f3ea06d9d8ffdd07d0d034b453d6495dd418c0 (patch) | |
| tree | be020e8948ae1a5d9313089462d081b5d5910a42 | |
| parent | 59ea396dc5fd01afd8f8dfd8ec18f84d787244c0 (diff) | |
Update compate Coq812.v
| -rw-r--r-- | theories/Compat/Coq812.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Compat/Coq812.v b/theories/Compat/Coq812.v index f52b559f84..992b00e834 100644 --- a/theories/Compat/Coq812.v +++ b/theories/Compat/Coq812.v @@ -11,4 +11,6 @@ (** Compatibility file for making Coq act similar to Coq v8.12 *) Require Export Coq.Compat.Coq813. +Local Set Warnings "-deprecated". Set Firstorder Solver auto with *. +Export Set Instance Generalized Output. |