Print type and environment of unsolved holes.

Was just printed in the case of internal holes.

Also: replace [str] by [strbrk] in error message of unsolved holes for better layout.
Adapting output/Arguments_renaming.out after fixing printing of
constants which without a @ would have a maximally inserted implicit
argument.
Revert "test-suite: New names for vars but the expected invariant is preserved"

This reverts commit cc06ffe3df0ecc023ad046a085b0751ed4161cbf.

Going back to the convention of naming bound variables in hypotheses
of the goal as in 8.4.

My arguments for the revert are:

- apply ... with (id:=...) would have to be changed too, then possibly
  breaking the compatibility
- the naming became dependent of the order of variables as in

x:nat
H:forall x0, x0=0
=====
goal

but

H:forall x, x=0
x:nat
=====
goal

Accordingly, this is all a matter of convention, since the meaning of
bindings is anyway the same in both cases.
Added make dependency in %.out in output tests.
Adapting the output test Notations:
- unbound variables in notation are allowed, forcing only parsing mode
- plus and mult are now themselves abbreviations
- evars are named
An evar name changed in output test.
Completing fixing order of parameters when translating from
glob_constr to constr_pattern. Was partially fixed to solve #3088
(8e88b7adab) in but the order of lambdas was still incorrect as the
fix of the order of lambdas in second-order pattern-matching for #3136
showed (83159124ce22).
Fixing bug #2810 (autounfold on local variable declared as hint but cleared).
Fixing interpretation of constr under binders which was broken after
it became possible to have binding names themselves bound to ltac
variables (2fcc458af16b).
Implement module subtyping for polymorphic constants (errors on
inductives).
The implementation constant should have the a universe instance
of the same length, we assume the universes are in the same order
and we check that the definition does not add any constraints
to the expected ones. This fixes bug #3670.
Adapting output/Arguments_renaming continued.
Fixing #3634 (wrong env in "cannot instantiate because not in its
scope" error message).
Add a bunch of reproduction files for bugs.
Fixing #3623 (unbound evars in types in a call to "change with").
Fixing ennoying warning about evars named ?23 and so on.
Test for bug #3652 fixed in 0fb36157b9ba
Fixing #3657 (check that both sides of a "change with" have the same
type, what is necessary condition to ensure that the conversion of
bodies will not raise an anomaly).
Removing deactivated command Show Tree.
Fixing #3606 continued (doc of Scheme Boolean Equality Scheme).
Classify segfaults as failures in opened bugs