coq - The formal proof system

Age	Commit message (Expand)	Author
2021-04-08	remove `with hintdb` variant of Ltac2 `unify`, because	Samuel Gruetter
2021-04-07	unify for Ltac2	Samuel Gruetter
2020-12-21	Move evaluable_global_reference from Names to Tacred.	Pierre-Marie Pédrot
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
2020-02-04	Fix #11515: Ltac2 rewrite on wildcard.	Pierre-Marie Pédrot
2019-07-08	[api] Deprecate GlobRef constructors.	Emilio Jesus Gallego Arias
2019-06-17	Update headers of files that were stuck on older headers.	Théo Zimmermann
2019-05-10	Make the check flag of conversion functions mandatory.	Pierre-Marie Pédrot
2019-05-07	Integrate build and documentation of Ltac2	Maxime Dénès