diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v index e29a22860f68e44a162e35c12d4a5cb4cc78ab32..cab53ecec4176b001d1e7a9e27df9ca99f6f4add 100644 --- a/tests/proofmode_ascii.v +++ b/tests/proofmode_ascii.v @@ -6,6 +6,10 @@ From iris.bi Require Import ascii. Set Default Proof Using "Type". +(* Remove this and the [Set Printing Raw Literals.] below once we require Coq +8.14. *) +Set Warnings "-unknown-option". + Section base_logic_tests. Context {M : ucmra}. Implicit Types P Q R : uPred M.