Frédéric Chyzak authored Nov 20, 2014 and Guillaume Melquiond committed Nov 21, 2014

• Omega now needs to be imported.
• Changes of names in the standard library: projT1 -> proj1_sig, projT2 ->
  proj2_sig, NPeano.Nat -> PeanoNat.Nat, existT -> exist.
• trunk exchanged the meanings of Rplus_lt_reg_l and Rplus_lt_reg_r, so that
  this swap was no longer needed in Rcomplements.  However, not all sources of
  Coquelicot did import Rcomplements, leading to some inconsistencies.
• A few “generalize (filter_and _ _ X Y)” no longer pass without filling one of
  the holes.  For the moment, they are marked as such (“Post-8.4 fix”), as I
  don't know if a better approach could be tried.  In a few cases, the added
  material could be kept short by posing a definition for a longish “(fun ... =>
  ...)”  earlier in the script.
• In a few other cases, trunk had seemingly become less powerful in order to be
  more consistent.  In particular the result of “refine” has changed, leading to
  a change in “evar_last” and of adding a “clearbody” or a “simpl” here and
  there.