From 9b897ac32a0e5937e72b18e4f007f3dbac290ef9 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 23 Apr 2026 12:44:10 +0200 Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/21947 --- test-suite/bugs/bug_3344.v | 1 + test-suite/bugs/bug_4187.v | 1 + 2 files changed, 2 insertions(+) diff --git a/test-suite/bugs/bug_3344.v b/test-suite/bugs/bug_3344.v index a5106b1f14..449a55f441 100644 --- a/test-suite/bugs/bug_3344.v +++ b/test-suite/bugs/bug_3344.v @@ -4,6 +4,7 @@ From Stdlib Require Import Ensembles. From Stdlib Require Import String. #[global] Set Implicit Arguments. #[global] Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Ltac clearbodies := repeat match goal with | [ H := _ |- _ ] => clearbody H end. Inductive Comp : Type -> Type := diff --git a/test-suite/bugs/bug_4187.v b/test-suite/bugs/bug_4187.v index d588346e14..27e7e91efc 100644 --- a/test-suite/bugs/bug_4187.v +++ b/test-suite/bugs/bug_4187.v @@ -3,6 +3,7 @@ (* coqc version 8.4pl5 (December 2014) compiled on Dec 28 2014 03:23:16 with OCaml 4.01.0 coqtop version 8.4pl5 (December 2014) *) Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. From Stdlib Require Import List.