From aed91a74d041ce8bcfec984851e3e12d9ad34f5f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Fri, 11 Jul 2025 17:22:01 +0200
Subject: [PATCH] Adapt to rocq-prover/rocq#20902 (induction checks the right
 scheme)

---
 test-suite/bugs/bug_2814.v | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/test-suite/bugs/bug_2814.v b/test-suite/bugs/bug_2814.v
index 73e8435149..8d9a1e050e 100644
--- a/test-suite/bugs/bug_2814.v
+++ b/test-suite/bugs/bug_2814.v
@@ -1,6 +1,7 @@
 From Stdlib Require Import Program.
 
-Goal forall (x : Type) (f g : Type -> Type) (H : f x ~= g x), False.
+Goal forall (x : Type) (f g : Type -> Type) (H : JMeq (f x) (g x)) (H:f x), g x.
   intros.
-  Fail induction H.
-Abort.
+  induction H.
+  assumption.
+Qed.