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-05-17	Ltac2: add notations for eval cbv in ... and other in place reductions	Michael Soegtrop

2020-05-03	Ensure eintros allows creating evars	Paolo G. Giarrusso
	Thread the `ev` (an `evar_flag`) appropriately through `intros0`. Discussed on https://gitter.im/coq/coq?at=5eacace7f0377f16316083b8.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2020-03-03	Ltac2: Add notation for enough and eenough	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.