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