coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Fixing an incompleteness of the ring/field tactics	amahboub	2013-08-23
*	Little fix for Nsatz: hypotheses not directly relevant to the nsatz	herbelin	2013-05-05
*	Restrict (try...with...) to avoid catching critical exn (part 15)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 7)	letouzey	2013-03-13
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	Array.create is deprecated	pboutill	2012-12-19
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	More cleanup in Ring_polynom and EnvRing	letouzey	2012-07-05
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05