Change handling of loadpath and mlpath.

- Option -I no longer handles loadpath, only mlpath. This is the same
  behavior as coq_makefile. Option -I-as is unchanged.
- Option -R no longer recursively adds to mlpath; only the root directory
  is added.
- user-contrib/ and xdg directories are no longer recursively added to
  the loadpath.
- theories/ and plugins/ are no longer recursively added to the loadpath
  when option -nois is passed.
- All the preconfigured directories are still recursively added to the
  mlpath though.
Add tool for fully qualifying Require statements.
Adding an [modify] function to the tactic monad. It allows to modify
the current state without having to use both get, bind and set.
Actually using the [modify] primitive.
Removing unused functions in Refiner.
Transfering the initial goals from the proofview to the proof object.
They were just passed along in the tactics.
Allowing proof view to be detached in CoqIDE.
Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. (Fix for Rocq/Rational.)
printer for coqchk
Fix universe handling (bug introduced in vi2vo commit)

Inside a section, Let followed by a Proof. Qed. are handled as regular
definitions, hence they have universe constraints coming from the type
and from the body.  Only the former set was returned to libstack, but
both sets were added to the global universe graph.  Hence, at section
closing time, an incomplete set of universe constraints was added back
to the global graph (End Section replays the libstack) and hence saved
in the .vo file.  coqchk was right in reporting missing constraints.
Add an option -Q (tentative name).

This option complements -I-as and -R. As the two other options, it adds a
new loadpath, but contrarily to them, files are not looked into the
directory unless fully qualified.
Uint31 support.
Int31 literals in native compiler.
Had to split Nativelambda in two files because of Retroknowledge
dependencies.
Partial support for open terms in int31.
Full support for int31 values in native compiler.
Readback for int31 values from native compiler.
Machine arithmetic operations for native compiler.

This completes the port of the native compiler to retroknowledge.
However, some testing and optimizations are still to be done.
Int31 decompilation in native compiler was still partial. Now fixed.
Optimizing Int31 support in native compiler, by not tagging
applications of I31 constructor as lazy.