coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-03-26	Fix Ltac2 `Array.init` exponential overhead	Jason Gross
	Previously, `Array.init` was computing the first element of the array twice, resulting in exponential overhead in the number of recursive nestings of `Array.init`. Notably, since `Array.map` is implemented in terms of `Array.init`, this exponential blowup shows up in any term traversal based on `Array.map` over the arguments of application nodes. Fixes #14011
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2020-02-08	Resolve #10342 : [Ltac2] Add array library	Michael Soegtrop

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-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.