lib/richPp: Fix a bug related to the compatibility with ocaml 3.12
  - The previous version of this module was using a feature of
    the Format module of ocaml 4.01.

  - Add comments.
lib/RichPp: Rename into Richpp.
printing/RichPrinter: Rename into Richprinter.
printing/{ppvernac, ppconstr, pptactic}: Rename RichPp into Richpp.
printing/Richprinter: Cosmetics.
Fixing compilation (name of module Richprinter) I partially feel
responsible about.
Removing "destruct" test not yet working.
Fixing bugs #3723 and #3787 (reinitialization of camlp5 empty levels)
by hopefully computing the right position where to reinit an empty
level. Also removing obsolete comment.
Test for bug #3723 and #3787 on reinitialization of empty camlp4/5 levels.
Dependency bug in using eqn for destruct.
Optimizing when to clear generalized hypotheses in destruct.

Removing blocking of generalization on destructed hypothesis
introduced on Nov 2. It was a bad idea as shown by bug #3790 on
eliminating v:Vector n, keeping an equality.
Restoring clear_flag (thanks a lot to jonikelee to notice it).
Consequence of changing the definition of Nat.shiftl and Nat.shiftr.
Print [rename] tactic properly in info trace.

Followup of d0a871374e3b3498c51d9d7b8e4510f7e1e7a3e1 (Writing rename_hyps in the new monad).
Removing the legacy intro tactic code.
doc: version number in cover.html + updates in coq.inria.fr style
Test for #3542 fixed some time ago.
Fixing #3562 ("as" in "destruct" expects either a disjunctive
intropattern or a bound ltac variable).
Test for #3675 on primitive projections.
Granting #3717 (more informative error message on missing arguments for functional induction).
Fixing Functional Induction when applied to an alias (reference manual
for Functional Induction was failing because of minus now an alias).

Knowing that minus is an alias for Sub.nat, there are still two bugs in
Functional Induction (Pierre or Julien?):

"Functional Scheme minus_ind := Induction for minus Sort Prop." is
failing when Nat is not imported.

"functional induction (minus n m)" is failing because looking for
sub_ind while the scheme is named minus_ind.
Fixing doc of Functional Induction.
Test fixed by PMP's commits from Oct 21.