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.
---
 coq | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'coq')

diff --git a/coq b/coq
index 0b04a8c7..fcf744fd 100755
--- a/coq
+++ b/coq
@@ -12,4 +12,4 @@ make -q ${1}o || {
    done)
 }
 
-"${COQBIN}coqide" $INCLUDES $1 && make ${1}o
+"${COQBIN}coqide" -async-proofs off $INCLUDES $1 && make ${1}o
-- 
cgit