Completing 5eb53b5bc8d765ed75e965f43f1084e18efc8790 (I unfortunately
did not notice that kernel/values.ml had to be made consistent with
kernel/cic.mli).
Native compiler: hide compiled files in a .coq-native subdirectory.
Injection: do not fail when arguments have sort Prop.

This historic limitation of the injection tactic does not seem to have any
precise justification. In fact, the only equalities that are not projectable is
when the arguments of the constructor have sort Set or Type and the inductive
type is in Prop (due to the restriction on pattern matching).

The command "Unset Injection On Proofs" restores the old behavior.
Trying to improve the error messages of injection.

Below are a few examples where the previous messages were misleading:

Module InProp.

Inductive tree : Prop := Leaf | Node : tree -> tree -> tree.

Variables x y : tree.

(* Wrong msg: "Nothing to do, it is an equality between convertible terms." *)
(* These terms are not convertible *)
Goal Node Leaf Leaf = Leaf -> False.
Fail intros H; injection H.
Abort.

End InProp.

Module InSet.

Inductive tree : Set := Leaf | Node : tree -> tree -> tree.

Variables x y : tree.

(* Wrong msg: "Not a projectable equality but a discriminable one." *)
(* This equality is both projectable and discriminable *)
Goal Node x (Node Leaf Leaf) = Node Leaf Leaf -> False.
intros H.
Fail injection H.
Abort.

End InSet.
Document changes on injection.
Fix Qcanon after changes on injection.
Fixing ml-doc.
Allowing the "Declare Instance" command anywhere. This was artificially
restricted to module types, although it was nothing more than a short hand
for Axiom + Existing Instance.
Update test-suite Makefile to handle coq-prog-args
Eta contractions to please cbn
Cbn is happier when ?SetPositive fixpoints have the set as recursive argument
Pos.iter arguments in a better order for cbn.