From 70e2ff37c3d3c6802d4b1903c2cdbf83c4f48c35 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 30 Jun 2026 16:08:45 +0200 Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/22192 --- theories/stripped_odd_order_theorem.v | 1 + 1 file changed, 1 insertion(+) diff --git a/theories/stripped_odd_order_theorem.v b/theories/stripped_odd_order_theorem.v index ce768e3..00fb323 100644 --- a/theories/stripped_odd_order_theorem.v +++ b/theories/stripped_odd_order_theorem.v @@ -20,6 +20,7 @@ Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2. Inductive equivalent P Q := Equivalent (P_to_Q : P -> Q) (Q_to_P : Q -> P). Inductive equal T (x : T) : T -> Type := Equal : equal T x x. +Scheme Rewriting for equal. (* Arithmetic *)