aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.mli
diff options
context:
space:
mode:
authorMaxime Dénès2019-04-25 14:09:42 +0200
committerMaxime Dénès2019-05-07 10:02:56 +0200
commit9779c0bf4945693bfd37b141e2c9f0fea200ba4d (patch)
tree26f563e3ad9562bdeb67efe8ff55be5de7fc55e2 /kernel/type_errors.mli
parent392d40134c9cd7dee882e31da96369dd09fbbb45 (diff)
Integrate build and documentation of Ltac2
Since Ltac2 cannot be put under the stdlib logical root (some file names would clash), we move it to the `user-contrib` directory, to avoid adding another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego. Thanks to @Zimmi48 for the thorough documentation review and the numerous suggestions.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions