coq - The formal proof system

Age	Commit message (Expand)	Author
2019-05-21	Remove definition-not-visible warning	Gaëtan Gilbert
2019-05-20	[Classes] Use prepare_parameter from DeclareDef.	Emilio Jesus Gallego Arias
2019-04-10	Functionalize env in type classes	Maxime Dénès
2019-03-27	[vernac] Thread proof state to declare_assumption for warning	Emilio Jesus Gallego Arias
2019-03-27	[vernac] Adapt to removal of imperative proof state.	Emilio Jesus Gallego Arias
2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
2019-02-22	Apply implicit binders to Hypothesis inside sections.	Jasper Hugunin
2019-02-20	Merge PR #9529: Change Primitive message: "is registered" -> "is declared".	Vincent Laporte
2019-02-17	Separate variance and universe fields in inductives.	Gaëtan Gilbert
2019-02-08	Change Primitive message: "is registered" -> "is declared".	Gaëtan Gilbert
2019-02-05	Make Program a regular attribute	Maxime Dénès
2019-02-04	Primitive integers	Maxime Dénès
2018-11-27	Merge PR #9046: Goptions.declare_* functions return unit instead of a write_f...	Emilio Jesus Gallego Arias
2018-11-24	Merge PR #8933: Make initial evar map argument to check_evars_are_solved opti...	Pierre-Marie Pédrot
2018-11-23	s/let _ =/let () =/ in some places (mostly goptions related)	Gaëtan Gilbert
2018-11-22	Deprecate Typeclasses Axioms Are Instances	Gaëtan Gilbert
2018-11-21	Make initial evar map argument to check_evars_are_solved optional.	Gaëtan Gilbert
2018-11-09	Adding universe names to polymorphic entry instances.	Pierre-Marie Pédrot
2018-10-16	{Univops -> Vars}.universes_of_constr	Gaëtan Gilbert
2018-10-16	UnivGen.constr_of_glob_univ -> Constr.mkRef	Gaëtan Gilbert
2018-10-05	Using smart mkLambdaCN/mkProdCN.	Hugo Herbelin
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-17	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert
2018-04-06	[api] Remove dependency of library on Vernacexpr.	Emilio Jesus Gallego Arias
2018-03-06	Rename some universe minimizing "normalize" functions to "minimize"	Gaëtan Gilbert
2018-03-05	Merge PR #6855: Update headers following #6543.	Maxime Dénès
2018-02-28	[econstr] Continue consolidation of EConstr API under `interp`.	Emilio Jesus Gallego Arias
2018-02-27	Update headers following #6543.	Théo Zimmermann
2018-02-22	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias
2017-12-17	[vernac] Split `command.ml` into separate files.	Emilio Jesus Gallego Arias