aboutsummaryrefslogtreecommitdiffstats
path: root/backend
diff options
context:
space:
mode:
Diffstat (limited to 'backend')
-rw-r--r--backend/PrintAsm.ml3
-rw-r--r--backend/PrintCminor.ml2
2 files changed, 2 insertions, 3 deletions
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index dd428808..155f5e55 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -13,7 +13,6 @@
open AST
open Camlcoq
-open DwarfPrinter
open PrintAsmaux
open Printf
open Sections
@@ -177,7 +176,7 @@ module Printer(Target:TARGET) =
let address = Target.address
end
- module DebugPrinter = DwarfPrinter (DwarfTarget)
+ module DebugPrinter = DwarfPrinter.DwarfPrinter (DwarfTarget)
end
let print_program oc p =
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index f68c1267..8c255a65 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -16,7 +16,7 @@
(** Pretty-printer for Cminor *)
open Format
-open Camlcoq
+open !Camlcoq
open Integers
open AST
open PrintAST