From e35365927d1289687aaff6d7ca5ebee1ac09d249 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 5 Feb 2020 17:40:02 +0100
Subject: add hint

---
 backend/CSE2proof.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 0d369e7a..0b92f5e5 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -358,6 +358,7 @@ Proof.
   discriminate.
   assumption.
 Qed.
+Local Hint Resolve wellformed_reg_kill_mem : wellformed.
 
 Lemma wellformed_mem_move:
   forall r dst rel,
-- 
cgit