From b4a08d0815342b6238d307864f0823d0f07bb691 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 26 May 2020 22:04:20 +0200
Subject: k1c -> kvx changes

---
 kvx/abstractbb/Impure/ImpExtern.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 kvx/abstractbb/Impure/ImpExtern.v

(limited to 'kvx/abstractbb/Impure/ImpExtern.v')

diff --git a/kvx/abstractbb/Impure/ImpExtern.v b/kvx/abstractbb/Impure/ImpExtern.v
new file mode 100644
index 00000000..8fb3cf3b
--- /dev/null
+++ b/kvx/abstractbb/Impure/ImpExtern.v
@@ -0,0 +1,7 @@
+(** Exporting Extern functions
+*)
+
+Require Export ImpPrelude.
+Require Export ImpIO.
+Require Export ImpLoops.
+Require Export ImpHCons.
-- 
cgit