coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\| \| *	congruence: remove casts of indexed terms	Matthieu Sozeau	2016-07-04
\| \| *	congruence/univs: properly refresh (fix #4609)	Matthieu Sozeau	2016-07-04
* \| \|	rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...	Pierre Letouzey	2016-07-03
* \| \|	closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)	Pierre Letouzey	2016-07-03
* \| \|	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
* \| \|	Add and document match, fix and cofix reduction flags.	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
\| * \|	Makefile: no bytecode compilation in make world, see make byte instead	Pierre Letouzey	2016-06-29
\|/ /
* \|	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-27
\|\\|
* \|	ssrmatching: avoid warnings about redundant typing clauses in ARGUMENT EXTEND	Pierre Letouzey	2016-06-27
* \|	Adding ability to put any pattern in binders, prefixed by a quote.	Daniel de Rauglaudre	2016-06-27
* \|	Removing tactic compatibility layers in setoid_ring.	Pierre-Marie Pédrot	2016-06-24
\| *	Fix typo.	Guillaume Melquiond	2016-06-23
* \|	Reuse the typing_flags datatype for inductives.	Pierre-Marie Pédrot	2016-06-18
* \|	Moving the typing_flags to the environment.	Pierre-Marie Pédrot	2016-06-18
* \|	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
* \|	Adding eintros to respect the e- prefix policy.	Hugo Herbelin	2016-06-18
* \|	Factorizing the uses of Declareops.safe_flags.	Pierre-Marie Pédrot	2016-06-16
* \|	Fixing a mispelling coma -> comma.	Hugo Herbelin	2016-06-16
* \|	Adding printers for ring and field commands.	Hugo Herbelin	2016-06-16