coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	end of correction of bug 4306	Julien Forest	2017-04-04
*	Bad correction in previous commit	Julien Forest	2017-04-04
*	Solving first problem in bug #4306. TO DO : solve the let in problem	Julien Forest	2017-04-04
*	Merge PR#495: funind: Ignore missing info for current function	Maxime Dénès	2017-03-23
\|\
* \|	Add empty Extraction.v and FunInd.v to prepare landing of PR#220.	Maxime Dénès	2017-03-23
\| *	funind: Ignore missing info for current function	Tej Chajed	2017-03-22
\|/
*	[ltac] Move dummy plugin to plugins folder.	Emilio Jesus Gallego Arias	2017-03-03
*	Extraction: fix complexity issue #5310	Pierre Letouzey	2017-02-07
*	ssrmatching: fix iter_constr_LR iterator wrt Proj	Enrico Tassi	2016-12-07
*	ssrmatching: handle primite projections (fix: #5247)	Enrico Tassi	2016-12-05
*	Fixing printers for pr_auto_using and pr_firstorder_using.	Hugo Herbelin	2016-12-02
*	Lazily load constants in micromega (bug #5134).	Guillaume Melquiond	2016-11-24
*	Merge commit 'e6edb33' into v8.6	Maxime Dénès	2016-11-07
\|\
* \	Merge remote-tracking branch 'github/pr/319' into v8.6	Maxime Dénès	2016-10-28
\|\ \
* \ \	Merge commit 'a799600' into v8.6	Maxime Dénès	2016-10-25
\|\ \ \
\| * \| \|	That Function is unable to create a Fixpoint equation is a user problem,	Yves Bertot	2016-10-25
* \| \| \|	ssrmatching: fix interpretation of rpattern	Enrico Tassi	2016-10-24
\|/ / /
\| \| *	Renamings to avoid confusion deprecating old names	Matthieu Sozeau	2016-10-22
\| \|/ \|/\|
\| *	[pp] Use more convenient pp API in ssrmatching	Emilio Jesus Gallego Arias	2016-10-18
\| *	[pp] Add tagging function to all low-level printing calls.	Emilio Jesus Gallego Arias	2016-10-18
\|/
*	Fix bug #5023: JSON extraction doesn't generate "for xxx".	Pierre-Marie Pédrot	2016-10-17
*	Ncring_initial: avoid a notation overriding	Pierre Letouzey	2016-09-29
*	Extraction: ignore some useless stuff about universes	Pierre Letouzey	2016-09-29
*	Ring_theory: avoid overriding a few notations	Pierre Letouzey	2016-09-28
*	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
*	Addressing OCaml compilation warnings.	Hugo Herbelin	2016-09-16
*	Fix Bug #5073 : regression of micromega plugin	Frédéric Besson	2016-09-08
*	Fix Bug #5073 : regression of micromega plugin	Frédéric Besson	2016-09-08
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-07
\|\
* \|	micromega : more robust generation of proof terms	Frédéric Besson	2016-09-07
\| *	Fixing what is probably a typo in Strict Proofs mode (#5062).	Hugo Herbelin	2016-09-03
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-02
\|\\|
* \|	Fixed Bug #5003 : more careful generalisation of dependent terms.	Frédéric Besson	2016-09-01
* \|	Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.	Frédéric Besson	2016-08-31
* \|	plugin micromega : nra also handles non-linear rational arithmetic over Q (Fi...	Frédéric Besson	2016-08-30
\| *	micromega cache files are now hidden files (cf #4156)	Frédéric Besson	2016-08-30
* \|	Make it a bit more obvious when variables are of type unit.	Guillaume Melquiond	2016-08-10
* \|	Reduce warning noise when compiling the standard library.	Guillaume Melquiond	2016-08-09
* \|	Fix bug #4923: Warning: appcontext is deprecated.	Pierre-Marie Pédrot	2016-07-18
* \|	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
\| \|/
* \|	Revert "Merge remote-tracking branch 'github/pr/229' into trunk"	Maxime Dénès	2016-07-05
\| *	Bug fix : variable capture in ltac code of Nsatz	thery	2016-07-05
* \|	Merge remote-tracking branch 'github/pr/229' into trunk	Maxime Dénès	2016-07-04
\|\ \
\| \| *	congruence: Restrict refreshing to Set	Matthieu Sozeau	2016-07-04