Fixing coqchk. It was my fault, I misused canonical and user equalities
when defining cache hash tables in Closure. Why it was working in 3.12
is a mystery to me.
Prevent verbatim text from leaking out of comments. (See bug #2882)
Closing bug #3164
Recognize "Instance" in coqwc. (Fix for bug #2551)
fixing Function doc
Fix for bug #3107.
closing bug 3037
Printers for ltac environments.
Fixing bug #3228 (fixing precedence of ltac variables over variables in env).
Test for bug #3142, actually duplicate of #3262.
Completing text of the question on conservativity of CIC over CC (bug #2697).
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