From 90418d09f172cdae37b66f78e3acd4c3cbc88b4f Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 19 Aug 2024 09:37:25 +0200
Subject: [PATCH] Compatibility with older versions of Coq

---
 backend/ValueDomain.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 05bf047d4..764fa2b12 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -4520,7 +4520,7 @@ Proof.
            id1 <> id2 -> b1 <> b2).
   { intros until id2; intros GE1 GE2 EQ1 EQ2 DIFF.
     apply GE1 in EQ1; apply GE2 in EQ2.
-    apply Genv.find_invert_symbol in EQ1, EQ2.
+    apply Genv.find_invert_symbol in EQ1; apply Genv.find_invert_symbol in EQ2.
     congruence. }
   assert (GLOB_STACK: forall (bc1 bc2: block_classification) ge sp b1 b2 id,
            genv_match bc1 ge -> bc1 sp = BCstack -> bc2 sp = BCstack ->