From 1bc8675a010cf410a9471fc2a0cecc86d48388d8 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 23 Apr 2026 13:19:34 +0200 Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/21947 --- theories/Model_RegExp.v | 1 + theories/Reification.v | 1 + theories/SemiRing.v | 1 + 3 files changed, 3 insertions(+) diff --git a/theories/Model_RegExp.v b/theories/Model_RegExp.v index 16bab84..4a7f997 100644 --- a/theories/Model_RegExp.v +++ b/theories/Model_RegExp.v @@ -30,6 +30,7 @@ From ATBR Require Import Reification. Set Implicit Arguments. Unset Strict Implicit. Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Module RegExp. diff --git a/theories/Reification.v b/theories/Reification.v index 62297c5..5774da5 100644 --- a/theories/Reification.v +++ b/theories/Reification.v @@ -17,6 +17,7 @@ From Stdlib Require Import Eqdep. Set Implicit Arguments. Unset Strict Implicit. Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. (* generic environments *) Definition sigma := PositiveMap.t. diff --git a/theories/SemiRing.v b/theories/SemiRing.v index 9feb2ab..1fa6f3f 100644 --- a/theories/SemiRing.v +++ b/theories/SemiRing.v @@ -26,6 +26,7 @@ From ATBR Require Import Reification. Set Implicit Arguments. Unset Strict Implicit. Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. #[global] Hint Extern 0 (equal _ _ _ _) => first [ apply dot_ann_left