coq - The formal proof system

Age	Commit message (Expand)	Author
2018-07-24	Add combinators to drop the bodies of local declarations.	Pierre-Marie Pédrot
2018-06-27	Swapping Context and Constr: defining declarations on constr in Constr.	Hugo Herbelin
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-04-20	correcting comments in the "Context" module	Matej Kosik
2017-02-14	Introducing contexts parameterized by the inner term type.	Pierre-Marie Pédrot
2016-08-26	CLEANUP: adding "Context.Compacted.Declaration.of_named_decl" function, which...	Matej Kosik
2016-08-26	CLEANUP: rename "Context.Named.{to,of}_rel" functions to "Context.Named.{to,o...	Matej Kosik
2016-08-26	CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"	Matej Kosik
2016-08-25	CLEANUP: changing the definition of the "Context.NamedList.Declaration" type	Matej Kosik
2016-08-25	CLEANUP: Type alias "Context.section_context" was removed	Matej Kosik
2016-08-25	CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...	Matej Kosik
2016-08-24	Merging a branch that adds "Context.Named.Declaration.to_rel" function.	Matej Kosik
2016-08-24	Adding "Context.Named.Declaration.to_rel" function	Matej Kosik
2016-08-17	Revert "CLEANUP: removing the definition of the "Context.Rel.Declaration.to_t...	Pierre-Marie Pédrot
2016-08-11	Adding "Context.Named.Declaraton.of_rel" function	Matej Kosik
2016-08-11	CLEANUP: removing the definition of the "Context.Rel.Declaration.of_tuple" fu...	Matej Kosik
2016-08-11	CLEANUP: removing the definition of the "Context.Rel.Declaration.to_tuple" fu...	Matej Kosik
2016-02-09	REFORMATTING: kernel/context.ml{,i}	Matej Kosik
2016-02-09	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2016-01-11	CLEANUP: kernel/context.ml{,i}	Matej Kosik
2015-12-05	Moving extended_rel_vect/extended_rel_list to the kernel.	Hugo Herbelin
2015-01-12	Update headers.	Maxime Dénès
2014-10-22	Pushing Pierre's factorization of names in goal context printing from	Hugo Herbelin
2014-10-20	A patch for printing "match" when constructors are defined with let-in	Hugo Herbelin
2014-09-01	Coqide prints succesive hyps of the same type on 1 line	Pierre Boutillier
2013-10-22	Removing some generic equalities.	ppedrot
2013-08-04	Removing useless casts between arrays and lists.	ppedrot
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot