From a78c3f9492c55b30409ae0e87b8df42062893482 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 4 Dec 2023 13:42:10 +0100 Subject: [PATCH] Silence warning in test --- tests/compiler_bug_14.v | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tests/compiler_bug_14.v b/tests/compiler_bug_14.v index edfe167..20ff5bc 100644 --- a/tests/compiler_bug_14.v +++ b/tests/compiler_bug_14.v @@ -4,6 +4,10 @@ Ltac2 test () := match mut with () => () end. From Ltac2Compiler Require Import Ltac2Compiler. +Set Warnings "+tac2compile-skipped-mutable". +Fail Ltac2 Compile test. + +Set Warnings "-tac2compile-skipped-mutable". Ltac2 Compile test. (* Dynlink error: execution of module initializers in the shared library failed: