Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to
one_inductive_body so that when eta-expanding at "match" printing time
we know if a let is part of the expected signature or part of the
body.

This is an easy fix for bugs like #3293. Another fix could be to
enforce, as an invariant, or better syntactically, that
"match"/"Case"'s have the body of their branches expanded.
Fixing #3293 (eta-expansion at "match" printing time was failing
because of let-in's interpreted as being part of the expansion).
Fixing coqdoc bug #3292 (unfortunate collision betweens the relative
locations found when parsing expressions in comments and the absolute
locations in the glob file).

As now, the glob file does not parse comment, so I removed the test
for location when parsing expressions in comments, which anyway are
not linkable, precisely because not parsed by coqc.
Fix incorrect syntax highlighting after the Goal command.
Fix broken commit 2bcb2cb.
Remove unused lookup table.
Mark lazymatch as an Ltac keyword for coqdoc. (Fix for bug #3276)
Recognize Parameters as a command in coqdoc. (Fix for bug #3279)
Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964)
Reduce the amount of "Coq <" prompts generated by coq_tex. (Partial fix for bug #2964)
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