From b8647d11c1af9bfe19fd8be33f8e88f92de77888 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 25 Nov 2020 13:48:18 +0100
Subject: store2_sound

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

(limited to 'backend/CSE3analysisproof.v')

diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 4c6b417c..b298ea65 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -1053,7 +1053,7 @@ Section SOUNDNESS.
     unfold store2.
     intros.
     destruct (Compopts.optim_CSE3_alias_analysis tt); eauto with cse3.
-  Admitted.
+  Qed.
   
   Hint Resolve store2_sound : cse3.
 
-- 
cgit