From 10da6dfa77f155d9d1e36e28c8bb8552601355f9 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Thu, 7 Jan 2021 18:21:55 +0100
Subject: update kvx

---
 kvx/Asmblockgenproof0.v | 1 -
 1 file changed, 1 deletion(-)

(limited to 'kvx/Asmblockgenproof0.v')

diff --git a/kvx/Asmblockgenproof0.v b/kvx/Asmblockgenproof0.v
index 1af59238..12bb863a 100644
--- a/kvx/Asmblockgenproof0.v
+++ b/kvx/Asmblockgenproof0.v
@@ -36,7 +36,6 @@ Require Import Asmblock.
 Require Import Asmblockgen.
 Require Import Conventions1.
 Require Import Axioms.
-Require Import Machblockgenproof. (* FIXME: only use to import [is_tail_app] and [is_tail_app_inv] *)
 Require Import Asmblockprops.
 
 Module MB:=Machblock.
-- 
cgit