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-12-21	Move evaluable_global_reference from Names to Tacred.	Pierre-Marie Pédrot
	It is the only place where it starts making sense in the whole codebase. It also fits nicely there since there are other functions manipulating this type in that module. In any case this type does not belong to the kernel.
2020-11-20	Granting #9816: apply in takes several hypotheses.	Hugo Herbelin

2020-03-31	Try only using TC for conversion in cominductive (not great but let's see)	Gaëtan Gilbert

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-04	Fix #11515: Ltac2 rewrite on wildcard.	Pierre-Marie Pédrot
	There was an evar leak due to an evarmap not being threaded correctly when computing open terms.
2019-07-08	[api] Deprecate GlobRef constructors.	Emilio Jesus Gallego Arias
	Not pretty, but it had to be done some day, as `Globnames` seems to be on the way out. I have taken the opportunity to reduce the number of `open` in the codebase. The qualified style would indeed allow us to use a bit nicer names `GlobRef.Inductive` instead of `IndRef`, etc... once we have the tooling to do large-scale refactoring that could be tried.
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-10	Make the check flag of conversion functions mandatory.	Pierre-Marie Pédrot
	The current situation is a mess, some functions set it by default, but other no. Making it mandatory ensures that the expected value is the correct one.
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.