coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert	2018-05-17
*	Make most of TACTIC EXTEND macros runtime calls.	Maxime Dénès	2018-03-08
*	[stdlib] Do not use “Require” inside sections	Vincent Laporte	2018-03-07
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle	2018-02-17
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[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
*	Merge PR#718: API cleanup: aliases	Maxime Dénès	2017-06-12
\|\
* \|	Remove remaining vo.itarget files (obsolete since PR #499)	Pierre Letouzey	2017-06-10
\| *	Remove (useless) aliases from the API.	Matej Košík	2017-06-10
\|/
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
*	Merge PR#512: [cleanup] Unify all calls to the error function.	Maxime Dénès	2017-05-29
\|\
\| *	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
* \|	[coqlib] Move `Coqlib` to `library/`.	Emilio Jesus Gallego Arias	2017-05-27
* \|	[coqlib] Deprecate redundant Coqlib functions.	Emilio Jesus Gallego Arias	2017-05-27
\|/
*	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
*	Remove some unused values and types	Gaetan Gilbert	2017-04-27
*	Remove unused [rec] keywords	Gaetan Gilbert	2017-04-27
*	Fix nsatz not recognizing real literals.	Guillaume Melquiond	2017-04-20
*	Merge PR#532: Clean Nsatz implementation.	Maxime Dénès	2017-04-11
\|\
\| *	Fix an algorithmic issue in Nsatz.	Pierre-Marie Pédrot	2017-04-09
\| *	Academic prescriptivism strikes back: down with baroque programming in Nsatz.	Pierre-Marie Pédrot	2017-04-09
* \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|\\|
\| *	Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun	Maxime Dénès	2017-03-14
\| \|\
\| * \|	Moving the Ltac plugin to a pack-based one.	Pierre-Marie Pédrot	2017-02-17
\| \| *	[cleanup] Change Id.t option to Name.t in TacFun	Tej Chajed	2017-02-16
\| \|/
* \|	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|/
*	Adding interface files to Nsatz ML files.	Pierre-Marie Pédrot	2016-09-28
*	Fast russian peasant exponentiation in Nsatz.	Pierre-Marie Pédrot	2016-09-26
*	Monomorphizing various uses of arrays in Nsatz.	Pierre-Marie Pédrot	2016-09-26
*	Partial fix for bug #5085: nsatz_compute stack overflows.	Pierre-Marie Pédrot	2016-09-26
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-07-13
\|\
* \	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-07-07
\|\ \
\| \| *	improved complexity in nsatz	thery	2016-07-06
\| \| *	Bug Fixes : 4851 4858 4880 for nsatz	thery	2016-07-06
\| \|/
\| *	Bug fix : variable capture in ltac code of Nsatz	thery	2016-07-05
* \|	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
* \|	Compilation via pack for plugins of the stdlib	Pierre Letouzey	2016-06-08
* \|	Put the "generalize" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
* \|	Splitting the nsatz ML module into an implementation and a grammar files.	Pierre-Marie Pédrot	2016-03-06
\|/
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Update headers.	Maxime Dénès	2015-01-12
*	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey	2014-12-09
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19