By default Coq stdlib warnings raise an error, so this is really required.

As noted by Hugo Herbelin, Dec is rather used for "decidable".

Previously rationals were all parsed as a pair numerator, denominator.
This means 1.02 and 102e-2 were both parsed as 102 # 100 and could not
be tell apart when printing. So the printer had to choose between two
representations : without exponent or without decimal dot. The choice
was made heuristically toward a most compact representation.

Now, decimal dot is still parsed as a power of ten denominator but
exponents are parsed as a product or division by Z.pow_pos. For
instance, 1.02 is parsed as 102 # 100 whereas 102e-2 is parsed as
(102 # 1) / (Z.pow_pos 10 2 # 1).

1.02 and 102e-2 remain equal (proved by reflexivity) but 1.02e1
= (102 # 100) * (10 # 1) = 1020 # 100 and 10.2 = 102 # 10 no longer are.

A nice side effect is that exponents can no longer blow up during
parsing. Previously 1e1_000_000 literally produced a numerator with a
million digits, now it just yields (1 # 1) * (Z.pow_pos 10 1_000_000 # 1).

This enables numeral notations for non inductive types by
pre/postprocessing them to a given proxy inductive type.
For instance, this should enable the use of numeral notations for R.

Similar to `dependent induction`, report an error message for `dependent
destruction` saying that importing `Coq.Program.Equality` is required,
rather than failing at parsing time.

This is a small extension of #605 to cover dependent destruction as
well. Here I also put in some tests.

Keep Numeral Notation wit a deprecation warning.

The apply <- tactic was breaking, so we had to modify the definition
in Init/Tactics.v to use slightly fresher names.