From be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Tue, 18 Feb 2020 16:57:17 +0100
Subject: Refine the type of function results in AST.signature

Before it was "option typ".  Now it is a proper inductive type
that can also express small integer types (8/16-bit unsigned/signed integers).

One benefit is that external functions get more precise types that
control better their return values.  As a consequence,
the CompCert C type preservation property now holds unconditionally,
without extra typing hypotheses on external functions.
---
 cfrontend/PrintCsyntax.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'cfrontend/PrintCsyntax.ml')

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
-- 
cgit