Updates for release 3.7

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`

doc/index.html

@@ -24,7 +24,7 @@
 
 <H1 align="center">The CompCert verified compiler</H1>
 <H2 align="center">Commented Coq development</H2>
-<H3 align="center">Version 3.6, 2019-09-17</H3>
+<H3 align="center">Version 3.7, 2020-03-31</H3>
 
 <H2>Introduction</H2>
 
@@ -101,6 +101,8 @@ <H3>Definitions and theorems used in many parts of the development</H3>
 <LI> <A HREF="html/compcert.common.Determinism.html">Determinism</A>: determinism properties of small-step semantics.
 <LI> <A HREF="html/compcert.powerpc.Op.html"><I>Op</I></A>: operators, addressing modes and their
 semantics.
+<LI> <A HREF="html/compcert.common.Builtins.html">Builtins</A>: semantics of built-in functions. <BR>
+See also: <A HREF="html/compcert.common.Builtins0.html">Builtins0</A> (target-independent part), <A HREF="html/compcert.powerpc.Builtins1.html"><I>Builtins1</I></A> (target-dependent part).
 <LI> <A HREF="html/compcert.common.Unityping.html">Unityping</A>: a solver for atomic unification constraints.
 </UL>