Fix bug due to shadowing a variable name in tacred
Make constrMatching and detyping more robust with respect to
expand_projection failing if an innapropriate sigma is given.
Add a "Debug Tactic Unification" option and correct the first-order
application case to expand primitive projections at the head of both
applications.
Add debug printers for projections, fix printing of evar constraints
and unsatisfiable constraints which were not done in the right environment.
Give the same argument name for the record binder of type class
projections and regular records.
Easily fixable backwards incompatibility.
Do not expand primitive projections eagerly in evarconv, but only
in cases of unification with existentials requiring it.
Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name
for the record binder of classes. This name is no longer generated
in the kernel but part of the declaration. Also cleanup the interface
to recognize primitive records based on an option type instead of a
dynamic check of the length of an array.
Tentative fix for a badly used Option.get in Reductionops.
Mentioning incompatibility shown in #3718 and coming from #3050
(interpreting "match goal"'s hypotheses in scope %type).
Coqinit: look in toploop/ even if configured with -local
library/opaqueTables: enable their use in interactive mode

Before this patch opaque tables were only growing, making them unusable
in interactive mode (leak on Undo).

With this patch the opaque tables are functional and part of the env.
I.e. a constant_body can point to the proof term in 2 ways:
  1) directly (before the constant is discharged)
  2) indirectly, via an int, that is mapped by the opaque table to
     the proof term.
This is now consistent in batch/interactive mode

This is step 0 to make an interactive coqtop able to dump a .vo/.vi
STM: simplify how the term part of a side effect is retrieved

Now the seff contains it directly, no need to force the future
or to hope that it is a Direct opaque proof.
TQueue: new primitive to take a snapshot of the queue
selective join/export of the safe_environment

This generalizes the BuildVi flag and lets one choose which
opaque proofs are done and which not.
STM: primitives to snapshot a .vi while in interactive mode
Parsing of "?[" as two tokens (makes ssr compile).

The problem is that "?[" makes the lexer glue "?" and "[" into
a single token but in ssr "?" (iteration) and "[" (rewrite pattern
delimiter) are often close, but they are parsed by very hard to
refactor grammar entries.

To consider:
- check the adjacency of the two symbols looking at the loc to
  parse exactly the same sentences as before this patch
- change syntax completely, e.g. "(_ as id)"
Emit a warning for void Arguments statement (Close 3713)
When loading libraries, feed back dependencies.

These dependencies between files can be used by UIs to guide compilation
and reloading of files.

FileDependency (Some "/foo.v", "/bar.v")  means foo depends on bar.
FileDependency (None, "/bar.v") means the current file depends on bar.
Stm: more precise representation of nested proofs

This fixes the bug reported by Hugo:
2)    Goal True.
3-4)  Definition a:=0.
5)    Goal True True.
(* jumped back to 3 (on master) instead of 4 (on the outermost proof) *)
Added support for several impossible cases in compilation of "match".