Updating versions history with data from Gérard.

Adding Gérard's history file about V1-V5 versions.

1 files changed, 40 insertions, 19 deletions

diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex
index fab6a37ef..1b1d3500a 100644
--- a/dev/doc/versions-history.tex
+++ b/dev/doc/versions-history.tex
@@ -10,55 +10,76 @@
 
 \begin{center}
 \begin{huge}
-An history of Coq versions
+A history of Coq versions
 \end{huge}
 \end{center}
 \bigskip
 
 \centerline{\large 1984-1989: The Calculus of Constructions}
+
+\bigskip
+\centerline{\large (see README.V1-V5 for details)}
 \mbox{}\\
 \mbox{}\\
 \begin{tabular}{l|l|l}
 version & date & comments \\
 \hline
-CoC V1.10& mention of dates from 6 December & implementation language is Caml\\
-         & 1984 to 13 February 1985 \\
 
-CoC V1.11& mention of dates from 6 December\\
-         & 1984 to 19 February 1985\\
+CONSTR V1.10& mention of dates from 6 December & \feature{type-checker for Coquand's Calculus }\\
+         & 1984 to 13 February 1985 & \feature{of Constructions}, implementation  \\
+         & frozen 22 December 1984 & language is a predecessor of CAML\\
+
+CONSTR V1.11& mention of dates from 6 December\\
+         & 1984 to 19 February 1985 (freeze date) &\\
+
+CoC V2.8& dated 16 December 1985 (freeze date)\\
 
-CoC V2.13& dated 16 December 1985\\
+CoC V2.9& & \feature{cumulative hierarchy of universes}\\
 
-CoC V2.13& dated 25 June 1986\\
+CoC V2.13& dated 25 June 1986 (freeze date)\\
 
-CoC V3.1& dated 20 November 1986 & \feature{auto}\\
+CoC V3.1& started summer 1986 & \feature{AUTO tactic}\\
+  & dated 20 November 1986 & implementation language now named CAML\\
 
 CoC V3.2& dated 27 November 1986\\
 
-CoC V3.3 and V3.4& dated 1 January 1987 & creation of a directory for examples\\
+CoC V3.3& dated 1 January 1987 & creation of a directory for examples\\
 
-CoC V4.1& dated 24 July 1987\\
+CoC V3.4& dated 1 January 1987 & \feature{lambda and product distinguished in the syntax}\\
+
+CoC V4.1& dated 24 July 1987 (freeze date)\\
 
 CoC V4.2& dated 10 September 1987\\
 
-CoC V4.3& dated 15 September 1987\\
+CoC V4.3& dated 15 September 1987 & \feature{mathematical vernacular toplevel}\\
+  & frozen November 1987 & \feature{section mechanism}\\
+  & & \feature{logical vs computational content (sorte Spec)}\\
+  & & \feature{LCF engine}\\
+
+CoC V4.4& dated 27 January 1988 & \feature{impredicatively encoded inductive types}\\
+  & frozen March 1988\\
 
-CoC V4.4& dated 27 January 1988\\
+CoC V4.5 and V4.5.5& dated 15 March 1988 & \feature{program extraction}\\
+  & demonstrated in June 1988\\
 
-CoC V4.5 and V4.5.5& dated 15 March 1988\\
+CoC V4.6& dated 1 September 1988 & start of LEGO fork\\
 
-CoC V4.6 and V4.7& dated 1 September 1988\\
+CoC V4.7& started 6 September 1988 \\
 
-CoC V4.8& dated 1 December 1988\\
+CoC V4.8& dated 1 December 1988 (release time) & \feature{floating universes}\\
 
-CoC V4.8.5& dated 1 February 1989\\
+CoC V4.8.5& dated 1 February 1989 & \\
 
-CoC V4.9& dated 1 March 1989\\
+CoC V4.9& dated 1 March 1989 (release date)\\
 
-CoC V4.10 and 4.10.1& dated 1 May 1989 & first public release - in English\\
+CoC V4.10 and 4.10.1& dated 1 May 1989 & released with documentation in English\\
 \end{tabular}
 
 \bigskip
+
+\noindent Note: CoC above stands as an abbreviation for {\em Calculus of
+  Constructions}, official name of the system.
+\bigskip
 \bigskip
 
 \newpage
@@ -80,7 +101,7 @@ Coq V5.2 & log dated 4 October 1990 & internal use \\
 
 Coq V5.3 & log dated 12 October 1990 & internal use \\
 
-Coq V5.4 & headers dated 24 October 1990 & internal use, \feature{extraction} (version 1) [3-12-90]\\
+Coq V5.4 & headers dated 24 October 1990 & internal use, new \feature{extraction} (version 1) [3-12-90]\\
 
 Coq V5.5 & started 6 December 1990 & internal use \\