From e2d7bba73f52285475da813433c703d7df7ae44a Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 27 Apr 2023 16:33:57 +0100
Subject: Update to Coq 8.17 and CompCert 3.12

---
 src/hls/DeadBlocksproof.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/hls/DeadBlocksproof.v')

diff --git a/src/hls/DeadBlocksproof.v b/src/hls/DeadBlocksproof.v
index 7f1da9c..107e206 100644
--- a/src/hls/DeadBlocksproof.v
+++ b/src/hls/DeadBlocksproof.v
@@ -544,7 +544,7 @@ Proof.
   elim H.
 
   intros.
-  elim not_seen_sons_prop6 with (1:=TT) (i0:=i); auto with datatypes.
+  eelim not_seen_sons_prop6 with (1:=TT) (i:=i); auto with datatypes.
   rewrite PTree.gsspec; destruct peq; subst; intros; auto with datatypes.
   rewrite PTree.gempty in H0; congruence.
 
-- 
cgit