From 94147eba46531a1bcaaa523b61eb0c77836afa3e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 23 Apr 2026 13:15:48 +0200 Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/21947 --- theories/AAC.v | 1 + theories/Utils.v | 1 + 2 files changed, 2 insertions(+) diff --git a/theories/AAC.v b/theories/AAC.v index adf74a2..287de83 100644 --- a/theories/AAC.v +++ b/theories/AAC.v @@ -34,6 +34,7 @@ From AAC_tactics Require Import Utils Constants. Set Implicit Arguments. Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope signature_scope. diff --git a/theories/Utils.v b/theories/Utils.v index 0e4a936..1bd51ca 100644 --- a/theories/Utils.v +++ b/theories/Utils.v @@ -12,6 +12,7 @@ From Stdlib Require Import Arith NArith List RelationClasses. Set Implicit Arguments. Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. (** ** Utilities for positive numbers