coq - The formal proof system

Age	Commit message (Collapse)	Author
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-12-12	Generalize the type of red_expr w.r.t. the type of flags they contain.	Pierre-Marie Pédrot

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 ml-style headers to new year.	Théo Zimmermann

2018-12-11	[api] Move reduction modules to `tactics`	Emilio Jesus Gallego Arias
	These modules do actually belong there. We have to slightly reorganize printers, removing a couple of duplicated ones in the way.