aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/PrintCsyntax.ml
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/PrintCsyntax.ml')
-rw-r--r--cfrontend/PrintCsyntax.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 1c9729c5..03dc5837 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -19,7 +19,7 @@ open Format
open Camlcoq
open Values
open AST
-open Ctypes
+open! Ctypes
open Cop
open Csyntax
@@ -85,7 +85,7 @@ let name_optid id =
let rec name_cdecl id ty =
match ty with
- | Tvoid ->
+ | Ctypes.Tvoid ->
"void" ^ name_optid id
| Ctypes.Tint(sz, sg, a) ->
name_inttype sz sg ^ attributes a ^ name_optid id