anchor.diff:  to Thierry Coquand.
   
   The programming language of the CONSTR software (as it was called at the time)
  -is a version of ML issued from the Edinburgh LCF system and running on
  -a LISP backend. The main improvements from the original LCF ML are that ML
  -is compiled rather than interpreted (Gérard Huet building on the original
  -translator by Lockwood Morris), and that it is enriched by recursively
  +was a version of ML adapted from the Edinburgh LCF system and running on
  +a LISP backend. The main improvements from the original LCF ML were that ML
  +was compiled rather than interpreted (Gérard Huet building on the original
  +translator by Lockwood Morris), and that it was enriched by recursively
   defined types (work of Guy Cousineau). This ancestor of CAML was used
   and improved by Larry Paulson for his implementation of Cambridge LCF.
   
  
positive.code: Version 4.5 was demonstrated in June 1988 at the YoP Institute on Logical
  Foundations of Functional Programming organized by Gérard Huet at Austin, Texas.
  
  Version 4.6 was started during summer 1988. Its main improvement was the
  complete rehaul of the proof synthesis engine by Thierry Coquand, with
  a tree structure of goals.
  
  
negative.code: Version 4.9 is released on March 1st 1989, with the new ``elastic''
  universe hierarchy.
  
  The spring of 1989 saw the first attempt at documenting the system usage,
  with a number of papers describing the formalism:
  
  - _Metamathematical Investigations of a Calculus of Constructions_, by
  