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".
English typo in a function name of evarconv.
Moving function about locs in locusops.
Naming main goal "Main"
Adding printers for ppproofview.
Adding a tactic which fails if one of the goals under focus is dependent in another one.
Add support for deactivating type class inference from induction/destruct.