coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Replace invalid tag @raises in ocamldoc comments with @raise	mrmr1993	2018-03-05
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Reductionops.nf_* now take an environment.	Gaëtan Gilbert	2018-02-02
*	Further clean-up in Reductionops, removing unused lift arguments.	Maxime Dénès	2017-12-12
*	[api] Remove yet another type alias.	Emilio Jesus Gallego Arias	2017-12-09
*	Getting rid of the Update constructor in Reductionops.	Pierre-Marie Pédrot	2017-12-06
*	Getting rid of the Shift constructor in Reductionops.	Pierre-Marie Pédrot	2017-12-06
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
*	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Fix a bug in cumulativity	Amin Timany	2017-06-16
*	Merge PR#714: Print feature Proof-of-Concept (episode 2)	Maxime Dénès	2017-06-13
\|\
* \|	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
\| *	Added support for a side effect on constants in reduction functions.	Thomas Sibut-Pinote	2017-06-04
\|/
*	Fix 4.04 warnings	Gaetan Gilbert	2017-04-27
*	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
*	Actually exporting delayed universes in the EConstr implementation.	Pierre-Marie Pédrot	2017-04-01
*	Make the Constr.kind_of_term type parametric in sorts and universes.	Pierre-Marie Pédrot	2017-03-31
*	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
*	Evar-normalizing functions now act on EConstrs.	Pierre-Marie Pédrot	2017-02-14
*	Cc API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Reductionops now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
*	Eliminating parts of the right-hand side compatibility layer	Pierre-Marie Pédrot	2017-02-14
*	Rewrite API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Inv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Clenv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Unification API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Pretyping 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
*	no-refold patch	Paul Steckler	2016-09-09
*	closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)	Pierre Letouzey	2016-07-03
*	Make semantics of whd_zeta consistent with other whd_* functions.	Maxime Dénès	2016-07-01
*	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
*	Using monotonic types for conversion functions.	Pierre-Marie Pédrot	2016-02-15
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	merge	Matej Kosik	2016-01-11
\|\ \
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	Remove duplicate declarations.	Guillaume Melquiond	2016-01-02
\|/ /
* /	CLEANUP: in the Reductionops module	Matej Kosik	2015-12-17
\|/
*	Avoid dependency of the pretyper on C code.	Maxime Dénès	2015-10-15
*	Fix #4346 2/2: VM casts were not inferring universe constraints.	Maxime Dénès	2015-10-15
*	Fix #4346 1/2: native casts were not inferring universe constraints.	Maxime Dénès	2015-10-15
*	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin	2015-08-02
*	Documenting in passing.	Hugo Herbelin	2015-08-02
*	Fix bug #3532, providing universe inconsistency information when a	Matthieu Sozeau	2015-03-04
*	Add support so that the type of a match in an inductive type with let-in	Hugo Herbelin	2015-02-27
*	Update headers.	Maxime Dénès	2015-01-12