aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-02-06 14:49:01 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2017-02-06 14:49:01 +0100
commit2543f6ecca50e930c23b705f6a3796ca05db85ff (patch)
tree6115fb439728633a3e6858d398d41fa023ac3d00 /exportclight
parent4e5a1b59c1653b1429f0a6cf2075ab2e54a43533 (diff)
downloadcompcert-kvx-2543f6ecca50e930c23b705f6a3796ca05db85ff.tar.gz
compcert-kvx-2543f6ecca50e930c23b705f6a3796ca05db85ff.zip
Removed shadowing open.
Diffstat (limited to 'exportclight')
-rw-r--r--exportclight/ExportClight.ml22
1 files changed, 11 insertions, 11 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index c4e373c0..003e97ee 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -18,9 +18,9 @@
open Format
open Camlcoq
open AST
-open !Ctypes
-open !Cop
-open !Clight
+open Ctypes
+open Cop
+open Clight
(* Options, lists, pairs *)
@@ -154,7 +154,7 @@ let rec typ p t =
and rtyp p = function
| Tvoid -> fprintf p "tvoid"
- | Tint(sz, sg, _) ->
+ | Ctypes.Tint(sz, sg, _) ->
fprintf p "%s" (
match sz, sg with
| I8, Signed -> "tschar"
@@ -164,12 +164,12 @@ and rtyp p = function
| I32, Signed -> "tint"
| I32, Unsigned -> "tuint"
| IBool, _ -> "tbool")
- | Tlong(sg, _) ->
+ | Ctypes.Tlong(sg, _) ->
fprintf p "%s" (
match sg with
| Signed -> "tlong"
| Unsigned -> "tulong")
- | Tfloat(sz, _) ->
+ | Ctypes.Tfloat(sz, _) ->
fprintf p "%s" (
match sz with
| F32 -> "tfloat"
@@ -279,7 +279,7 @@ let name_binop = function
| Oshl -> "Oshl"
| Oshr -> "Oshr"
| Oeq -> "Oeq"
- | One -> "One"
+ | Cop.One -> "One"
| Olt -> "Olt"
| Ogt -> "Ogt"
| Ole -> "Ole"
@@ -541,14 +541,14 @@ let print_program p prog =
fprintf p "@[<v 0>";
fprintf p "%s" prologue;
define_idents p;
- List.iter (print_globdef p) prog.prog_defs;
+ List.iter (print_globdef p) prog.Ctypes.prog_defs;
fprintf p "Definition composites : list composite_definition :=@ ";
print_list print_composite_definition p prog.prog_types;
fprintf p ".@ @ ";
fprintf p "Definition prog : Clight.program := {|@ ";
- fprintf p "prog_defs :=@ %a;@ " (print_list print_ident_globdef) prog.prog_defs;
- fprintf p "prog_public :=@ %a;@ " (print_list ident) prog.prog_public;
- fprintf p "prog_main := %a;@ " ident prog.prog_main;
+ fprintf p "prog_defs :=@ %a;@ " (print_list print_ident_globdef) prog.Ctypes.prog_defs;
+ fprintf p "prog_public :=@ %a;@ " (print_list ident) prog.Ctypes.prog_public;
+ fprintf p "prog_main := %a;@ " ident prog.Ctypes.prog_main;
fprintf p "prog_types := composites;@ ";
fprintf p "prog_comp_env := make_composite_env composites;@ ";
fprintf p "prog_comp_env_eq := refl_equal _@ ";