From 0471b29ce6de7dfb4f44f4ceec76251e35934aec Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Mon, 6 Feb 2017 14:01:04 +0100
Subject: Remove unused open

---
 powerpc/TargetPrinter.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'powerpc/TargetPrinter.ml')

diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 3d4db98f..68cd001b 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -14,7 +14,6 @@
 
 open Printf
 open Fileinfo
-open !Datatypes
 open Maps
 open Camlcoq
 open Sections
-- 
cgit