diff options
| author | Maxime Dénès | 2019-04-25 14:09:42 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-05-07 10:02:56 +0200 |
| commit | 9779c0bf4945693bfd37b141e2c9f0fea200ba4d (patch) | |
| tree | 26f563e3ad9562bdeb67efe8ff55be5de7fc55e2 /kernel/type_errors.mli | |
| parent | 392d40134c9cd7dee882e31da96369dd09fbbb45 (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
