aboutsummaryrefslogtreecommitdiff
path: root/user-contrib/Ltac2/tac2extffi.ml
AgeCommit message (Collapse)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2019-06-17Update headers of files that were stuck on older headers.Théo Zimmermann
Most of these files were introduced after #6543 but used older headers copied from somewhere else.
2019-05-07Integrate build and documentation of Ltac2Maxime Dénès
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.