coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-04-08	remove `with hintdb` variant of Ltac2 `unify`, because	Samuel Gruetter
	passing one single hintdb is not quite the right API, we should pass a transparent state instead, but that would require an API for manipulating hintdbs and transparent states, postponing
2021-04-07	unify for Ltac2	Samuel Gruetter
	Fixes #14083
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-06-17	Update 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-06-16	Fix #10090: Ltac1 destruct and Ltac2 destruct should do the same thing.	Pierre-Marie Pédrot
	The ML wrapper was wrongly calling induction instead of destruct.
2019-05-07	Integrate build and documentation of Ltac2	Maxime 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.