Fix missing lift in VM and native compiler (second part of #2729).

Was occurring in the parameters of constructors when reifying a dependent
pattern matching return predicate. Note: this does not affect the kernel,
only the pretyper.
Fix test-suite for #2729.

Was always failing due to an incorrect use of Ltac's or.
Move 'Arguments: clear implicits' to 2.7.4 (Close 2891)
Goal printing made uniform: always done in STM (close 3585)

Goal printing was partially broken.  Some commands in vernacentries
were printing, but not all of them.  Moreover an unlucky combination
of `Flags.verbosely (fun () -> interp "Set Silent")` was making the
silent flag not settable anymore.

Now STM always print the open goals after a command when run in interactive
mode via coqtop or emacs.  More modern GUI do ask for the goals.
Fix the way lexeme start is computed (Close 3737)
Make rint_location_in_file resilient to Cd (close 3630)

Cd can make the relative path of the opened file wrong,
and hence not available anymore when we reopen it to compute
the line number.
Specializing tclBREAK so that it can choose the return exception in case
of a break.
CoqIDE: fix parsing of multicharacter bullets
Removing an unused variant of Context.fold_named_context_reverse.
Pushing Pierre's factorization of names in goal context printing from
coqide to coqtop.

(Joint work with Pierre)
Fixing typo in output test Notations.
Bugfix 3604 : more robust Unix.lockf
Proofview: forgot to change an exception after refactoring in ( 9f51aafebd5f3a00dabfe056772a300830b3c430 )
Evd.future_goals: forgot to revert the list in two places.
Monad: change the error managing of two-list combinators.

Otherwise I risked catching errors from the argument functions when I wanted to catch size mismatch to add information to errors.
An API for info traces.
TEMP! Print info trace on all tactics.
Idtac logs its message in the info trace.
Add a interpreted level [tacexpr] to [Tacexpr].
Add a printer for [Tacexpr.tacexpr] in [Pptactic].

Adapted from the v8.3