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) *)