coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias	2017-12-23
*	[vernac] Split `command.ml` into separate files.	Emilio Jesus Gallego Arias	2017-12-17
*	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias	2017-11-21
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
*	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
*	Detyping functions are now operating on EConstr.t.	Pierre-Marie Pédrot	2017-08-01
*	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Fix bugs and add an option for cumulativity	Amin Timany	2017-06-16
*	Remove (useless) aliases from the API.	Matej Košík	2017-06-10
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
*	Cleanup: removal of constr_of_global.	Matthieu Sozeau	2017-05-29
*	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
\| *	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
* \|	[location] [ast] Port module AST to CAst	Emilio Jesus Gallego Arias	2017-04-25
* \|	[location] [ast] Switch Constrexpr AST to an extensible node type.	Emilio Jesus Gallego Arias	2017-04-25
* \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
* \|	[location] Switch glob_constr to Loc.located	Emilio Jesus Gallego Arias	2017-04-24
* \|	[location] Use Loc.located for constr_expr.	Emilio Jesus Gallego Arias	2017-04-24
\|/
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-04-04
\|\
* \|	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
\| *	Replacing "cast surgery" in LetIn by a proper field (see PR #404).	Hugo Herbelin	2017-03-24
\| *	Unifying standard "constr_level" names for constructors of local_binder_expr.	Hugo Herbelin	2017-03-24
* \|	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
* \|	Removing some return type compatibility layers in Termops.	Pierre-Marie Pédrot	2017-02-14
* \|	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Reductionops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Termops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|/
*	CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".	Matej Kosik	2016-10-19
*	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\
* \|	CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...	Matej Kosik	2016-08-30
* \|	CLEANUP: taking advantage of "_ % _" operator to express function composition...	Matej Kosik	2016-08-29
* \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
\| *	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
\| *	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias	2016-08-19
\|/
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Reuse the typing_flags datatype for inductives.	Pierre-Marie Pédrot	2016-06-18
*	Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.	Pierre-Marie Pédrot	2016-06-16
\|\
* \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
* \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\ \
\| * \|	Update copyright headers.	Maxime Dénès	2016-01-20
* \| \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
\|/ /
* \|	Univs: local names handling.	Matthieu Sozeau	2015-10-28
* \|	Fix some typos.	Guillaume Melquiond	2015-10-13
* \|	Univs: Add universe binding lists to definitions	Matthieu Sozeau	2015-09-14
\| *	Add corresponding field in `VernacInductive`.	Arnaud Spiwack	2015-06-24
\|/