Relax a bit the guard condition.

My previous optimization of guard checking (f1280889) made it slightly stricter,
in the presence of dependent pattern matching and nested inductive types whose
toplevel types are mutually recursive.

The following (cooked-up) example illustrates this:

Inductive list (A B : Type) := nil : list A B | cons : A -> list A B -> list
A B.

Inductive tree := Node : list tree tree -> tree.

Lemma foo : tree = tree. exact eq_refl. Qed.

Fixpoint id (t : tree) :=
  match t with
  | Node l =>
    let l := match foo in (_ = T) return list tree T with eq_refl => l end
    in
    match l with
    | nil  => Node (nil _ _)
    | cons x tl => Node (cons _ _ (id x) tl)
    end
  end.

is accepted, but changing tree to:

Inductive tree := Node : list tree tree -> tree.
with tree2 := .

made id be rejected after the optimization.

The same problem occurred in Paco, and is now fixed.

Note that in the example above, list cannot be mutually recursive because of the
current strict positivity condition for tree.
Port last changes of the guard condition to checker.
Removing the "constructor" tactic from the AST.
Instead of relying on a trick to make the constructor tactic parse, put
all the tactics using the constructor keyword in one entry. This has the
side-effect to also remove the other variant of constructor from the AST.

I also needed to hack around the "tauto" tactic to make it work, by
calling directly the ML tactic through a TacExtend node. This may be
generalized to get rid of the intermingled dependencies between this
tactic and the infamous Ltac quotation mechanism.
Removing simple induction / destruct from the AST.
In Hipattern: some functions not working modulo evar instantiation.

In theory [Proofview.Goal.env] should be, itself, marked as requiring a normalised goals (as it includes [hyps] which does). However, it is impractical as it is very common to pass a goal environment to a function reasoning modulo evars. So I guess we are bound to mark the appropriate functions by hand.
Hypotheses in [Proofview.Goal.enter] were not normalised.

Fixes PTSF (though I have no idea what caused this bug to show up just yesterday).
Add some more entries to .mailmap
More .mailmap update.
Better structure for Ltac pretyping environments.
Fix evarconv not applying eta when it used to. Fixes bug#3319.
Change internalization of primitive projections to allow parsing [p t] as
a primitive application only if all parameters of [p] are implicit, falling
back to the internalization of the eta-expanded version otherwise. This makes
apply [p] succeed even if its record argument is not implicit, ensuring better
compatibility.
First step towards [info]
An API for [info].
TEMP! Print info trace on all tactics.
Idtac logs its message in the info trace.
[idtac] does not add a new line in the trace.
Don't print empty comment for atomic tactics.
Simplistic printing of the [glob_tactic_expr] for the trace of atomic tactics.
Add a interpreted level [tacexpr] to [Tacexpr].