From 5a425ba34f3f2520de752ea95a4636a9437c312a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 22 Mar 2019 08:12:41 +0100
Subject: ça recompile sur x86
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 x86/SelectLongproof.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'x86/SelectLongproof.v')

diff --git a/x86/SelectLongproof.v b/x86/SelectLongproof.v
index 3bef632d..f008f39e 100644
--- a/x86/SelectLongproof.v
+++ b/x86/SelectLongproof.v
@@ -16,6 +16,7 @@ Require Import String Coqlib Maps Integers Floats Errors.
 Require Archi.
 Require Import AST Values Memory Globalenvs Events.
 Require Import Cminor Op CminorSel.
+Require Import OpHelpers OpHelpersproof.
 Require Import SelectOp SelectOpproof SplitLong SplitLongproof.
 Require Import SelectLong.
 
-- 
cgit