Restored old behavior of injection on proofs by default.

Use Set Injection On Proof to enable the new behavior.
Suggest Set Injection On Proofs in error message for injection.
When discrimination is not possible, try to project.

Example:
Inductive Pnat : Prop := O | S : Pnat -> Pnat.

Variable m n : Pnat.

Goal S (S O) = S O -> False.
intros H; injection H.

now deduces S O = O instead of failing with an error message.
Revert "Fix Qcanon after changes on injection."

This reverts commit f3b3b6e4d01080da4f0ce37a06553769e9588d0e.
Tentative to add constr-using primitive tactics without grammar rules.
We eta-expand primitive Ltac functions, and instead of feeding TacExtend
directly with its arguments, we use the environment to retrieve them.

Some tactics from the AST were also moved away and made using this
mechanism.
Tactics declared through TACTIC EXTEND that are of the form

"foobar" constr(x1) ... constr(xn)

are now defined as pure Ltac definitions, and do not add grammar
nor printing rules. This partially relies on a hack consisting
in retrieving the arguments in the tactic environment rather than
as directly passed to the TacExtend node.
Moving (e)transitivity out of the AST.
Moving left & right tactics out of the AST.
Allowing Ltac definitions that may be unusable because of a built-in
parsing rule.
Removing decompose record / sum from the tactic AST.
Removing useless use of metaids in tactic AST.
Ignore generated file.
Fix native_compute for systems with a limited size for the command line.

The call to the native compiler can fail due to the sheer amounts of -I
options passed to it. Indeed, it is easy to get the command line to exceed
512KB, thus causing various operating systems to reject it. This commit
avoids the issue by only passing the -I options that matter for the
currently compiled code.

Note that, in the worst case, this commit is still not sufficient on
Windows (32KB max), but this worst case should be rather uncommon and thus
can be ignored for now.

For the record, the command-line size mandated by Posix is 4KB.
Moving the "specialize" tactic out of the AST. Also removed an obsolete
variant of it, accepting an additional integer.
Complying with reference manual for the syntax of exists/eexists, i.e.
removing the strange kind of syntax "exists ,t,". which was equivalent to
"split; exists t; split", as in e.g.:

Goal (exists x, x=0) /\ (exists x, x=0).
exists ,0,.
Qed.

This answers bug request #3340.
Fixing TACTIC EXTEND for arguments-free tactics that may modify the whole
proof. Indeed, computing an empty list of arguments triggered a
Proofview.Goal.enter, which broke tactics like [shelve_unifiable].

This does not fix this particular tactic though, because the Ltac
interpreter still enters the goal when calling a Ltac reference.
Chasing the goal entering backward while interpreting tactics. This required
writing a new primitive recovering the first goal under focus. It sounds a bit
hackish, but it does actually work.
Revert "Chasing the goal entering backward while interpreting tactics. This required"
I tested the commit on the wrong branch...

This reverts commit b0364eff4ec8ad5676060d8ca9cdbbb1d9c34d04.
Fixing commit 9cef834. The parsing rules were generating an empty list,
conflicting with the previous behaviour of 'eexists'.
make coqdep canonicalize paths from the command line

- logical paths given to -R and -I should be split
  on periods.
- it also seems like giving an empty string should
  result in the empty path rather than the singleton
  path with an empty string as an identifier.