coq - The formal proof system

Age	Commit message (Expand)	Author
2018-10-16	Merge PR #8059: Simplify code for [Definition := Eval ...]	Matthieu Sozeau
2018-10-11	[vernac] Remove unused abstraction from declaration_hook type.	Emilio Jesus Gallego Arias
2018-10-09	Simplify code for [Definition := Eval ...]	Gaëtan Gilbert
2018-06-26	universes_of_constr don't include universes of monomorphic constants	Gaëtan Gilbert
2018-05-31	[api] Move `Constrexpr` to the `interp` module.	Emilio Jesus Gallego Arias
2018-05-25	Remove some occurrences of Evd.empty	Maxime Dénès
2018-05-07	[vernac] taint two out-of-api `to_constr` use in `comDefinition`.	Emilio Jesus Gallego Arias
2018-03-31	[econstr] Forbid calling `to_constr` in open terms.	Emilio Jesus Gallego Arias
2018-03-06	Rename some universe minimizing "normalize" functions to "minimize"	Gaëtan Gilbert
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-12-21	Merge code paths in interp_definition and cleanup a bit.	Gaëtan Gilbert
2017-12-18	[vernac] Cleanup of do_definition.	Emilio Jesus Gallego Arias
2017-12-17	[flags] Make program_mode a parameter for commands in vernac.	Emilio Jesus Gallego Arias
2017-12-17	[vernac] Split `command.ml` into separate files.	Emilio Jesus Gallego Arias