From ca42ad21fe033f8ed31c168a0d1fd46a51eefc2c Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Mon, 6 Feb 2017 13:41:12 +0100
Subject: Inline open Datatypes.

---
 x86/TargetPrinter.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index b5aeefae..5fb8ae0c 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -13,7 +13,6 @@
 (* Printing x86-64 assembly code in asm syntax *)
 
 open Printf
-open !Datatypes
 open Camlcoq
 open Sections
 open AST
@@ -244,9 +243,9 @@ module Target(System: SYSTEM):TARGET =
 
     let addressing_gen ireg oc (Addrmode(base, shift, cst)) =
       begin match cst with
-      | Coq_inl n ->
+      | Datatypes.Coq_inl n ->
           fprintf oc "%s" (Z.to_string n)
-      | Coq_inr(id, ofs) ->
+      | Datatypes.Coq_inr(id, ofs) ->
           if Archi.ptr64 then begin
             (* RIP-relative addressing *)
             let ofs' = Z.to_int64 ofs in
-- 
cgit