From 6dace9be5f4760882f879d3026c168cc9112e150 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 31 Mar 2020 17:48:34 +0200 Subject: Updates for release 3.7 --- Changelog | 3 +++ doc/index.html | 4 +++- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/Changelog b/Changelog index 9dc858ca..8cf4e548 100644 --- a/Changelog +++ b/Changelog @@ -1,3 +1,6 @@ +Release 3.7, 2020-03-31 +======================= + ISO C conformance: - Functions declared `extern` then implemented `inline` remain `extern` - The type of a wide char constant is `wchar_t`, not `int` diff --git a/doc/index.html b/doc/index.html index 3a4cf6ba..631c5d99 100644 --- a/doc/index.html +++ b/doc/index.html @@ -24,7 +24,7 @@ a:active {color : Red; text-decoration : underline; }

The CompCert verified compiler

Commented Coq development

-

Version 3.6, 2019-09-17

+

Version 3.7, 2020-03-31

Introduction

@@ -101,6 +101,8 @@ See also: Memdata (in-memory rep
  • Determinism: determinism properties of small-step semantics.
  • Op: operators, addressing modes and their semantics. +
  • Builtins: semantics of built-in functions.
    +See also: Builtins0 (target-independent part), Builtins1 (target-dependent part).
  • Unityping: a solver for atomic unification constraints. -- cgit