Adapt to https://github.com/rocq-prover/rocq/pull/21947

theories/AAC.v

@@ -34,6 +34,7 @@
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope signature_scope.
 
@@ -260,7 +261,7 @@
      contains, among other things, the arity of symbols).
    *)
 
   Inductive T: Type :=
   | sum: idx -> mset T -> T
   | prd: idx -> nelist T -> T
   | sym: forall i, vT (Sym.ar (e_sym i)) -> T

theories/Utils.v

@@ -12,6 +12,7 @@
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 (** ** Utilities for positive numbers
 
@@ -20,7 +21,7 @@
   - multiplicity of terms in sums
 *)
 
 Notation idx := positive.
 
 Fixpoint eq_idx_bool i j :=
   match i,j with
@@ -65,7 +66,7 @@
 
 (** ** Dependent types utilities *)
 
 Notation cast T H u := (eq_rect _ T u _ H).
 
 Section dep.
   Variable U: Type.
@@ -127,7 +128,7 @@
 Definition mset A := nelist (A*positive).
 
 (** Lexicographic composition of comparisons (this is a notation to keep it lazy) *)
 Notation lex e f := (match e with Eq => f | _ => e end).
 
 Section lists.