coq/test-suite/ltac2/stuff, branch master The formal proof system Integrate build and documentation of Ltac2 2019-05-07T08:02:56+00:00 Maxime Dénès 2019-04-25T12:09:42+00:00 9779c0bf4945693bfd37b141e2c9f0fea200ba4d 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. 
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.