coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Moving Ltac-specific parsing API to ltac/ folder.	Pierre-Marie Pédrot	2016-09-14
*	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\
* \	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-07
\|\ \
\| * \	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.6'	Pierre-Marie Pédrot	2016-09-02
\|\\| \| \|
\| * \| \|	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
* \| \| \|	CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...	Matej Kosik	2016-08-30
* \| \| \|	CLEANUP: using \|> operator more consistently	Matej Kosik	2016-08-30
* \| \| \|	CLEANUP: taking advantage of "_ % _" operator to express function composition...	Matej Kosik	2016-08-29
* \| \| \|	CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...	Matej Kosik	2016-08-25
* \| \| \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
* \| \| \|	CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" function	Matej Kosik	2016-08-24
* \| \| \|	CLEANUP: removing unnecessary variable binding	Matej Kosik	2016-08-24
\| \| \| *	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
\| \| \| *	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias	2016-08-19
\| \| \| *	Unify location handling of error functions.	Emilio Jesus Gallego Arias	2016-08-19
\| \|_\|/ \|/\| \|
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-08-17
\|\\| \|
* \| \|	CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" function	Matej Kosik	2016-08-11
\| * \|	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