anchor.diff:  Version 4.9 is released on March 1st 1989, with the new ``elastic''
   universe hierarchy.
   
  -The spring 89 saw the first attempt at documenting the system usage,
  +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
  
positive.code: Mathematics_. Invited paper, EUROCAL85, April 1985, Linz, Austria. Springer Verlag
  LNCS 203, pp. 151-184.
  
  Christine Paulin joined the team at this point, for her DEA research internship.
  In her DEA memoir (August 1985) she presents developments for the _lambo_ function
  computing the minimal _m_ such that _f(m)_ is greater than _n_, for _f_ an increasing
  integer function, a challenge for constructive mathematics. She also encoded
  the majority voting algorithm of Boyer and Moore.
  
  Version 2
  
negative.code: it was entirely re-checked by the engine. Thus there was no need to certify
  the tactics, and the system took advantage of this fact by having tactics ignore
  the universe levels, universe consistency check being relegated to the final
  type-checking pass. This induced a certain puzzlement in early users who saw,
  after a successful proof search, their `QED` followed by silence, followed by
  a failure message due to a universe inconsistency…
  
  The set of examples comprise set theory experiments by Hugo Herbelin,
  and notably the Schroeder-Bernstein theorem.
  