coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Proofview.Goal.sigma returns an indexed evarmap.	Pierre-Marie Pédrot	2015-10-20
*	Indexing Proofview.goals with a stage.	Pierre-Marie Pédrot	2015-10-20
*	Boxing the Goal.enter primitive into a record type.	Pierre-Marie Pédrot	2015-10-20
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|\
* \|	Type delayed_open_constr is now monotonic.	Pierre-Marie Pédrot	2015-10-19
* \|	Function debug mode more formatted.	Pierre Courtieu	2015-10-19
\| *	Partly fixes #3225. Removed some old experimental stuff in funind.	Pierre Courtieu	2015-10-19
* \|	Constraining refine to monotonic functions.	Pierre-Marie Pédrot	2015-10-18
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Exporting the original unprocessed hint in the hint running function.	Pierre-Marie Pédrot	2015-10-14
\| *	Fix some typos.	Guillaume Melquiond	2015-10-13
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\|
\| *	f_equal fix continued: do a refresh_universes as before.	Matthieu Sozeau	2015-10-08
\| *	Fix bug #4069: f_equal regression.	Matthieu Sozeau	2015-10-07
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\\|
\| *	Univs: fix after rebase (from_ctx/from_env)	Matthieu Sozeau	2015-10-02
\| *	Univs: fix evar_map initialization in newring.	Matthieu Sozeau	2015-10-02
\| *	Univs: fix evar_map leaks bugs in Function	Matthieu Sozeau	2015-10-02
\| *	Univs: fix an evar leak in congruence	Matthieu Sozeau	2015-10-02
* \|	Removing uselessly duplicated function in Evd.	Pierre-Marie Pédrot	2015-09-27
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-09-17
\|\\|
\| *	Univs: Add universe binding lists to definitions	Matthieu Sozeau	2015-09-14
* \|	Opacifying the proof_terminator type.	Pierre-Marie Pédrot	2015-09-08
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-09-06
\|\\|
\| *	Improve directives for Haskell extraction of nat.	Maxime Dénès	2015-09-03
\| *	Fix [Z.div] and add [Z.modulo] in ExtrHaskellZNum.v	Nickolai Zeldovich	2015-09-03
\| *	Fix [Nat.div] and add [Nat.modulo] in ExtrHaskellNatNum.v	Nickolai Zeldovich	2015-09-03
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-27
\|\\|
\| *	Extraction: fix primitive projection extraction.	Matthieu Sozeau	2015-07-22
* \|	Merge branch 'v8.5' into trunk	Pierre Letouzey	2015-06-22
\|\\|
\| *	Add efficient extraction of [nat], [Z], and [string] to Haskell	Nickolai Zeldovich	2015-06-22
* \|	micromega : fix silly timeout	Frédéric Besson	2015-06-06
* \|	micromega : options to limit proof search	Frédéric Besson	2015-05-26
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\|
\| *	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
\| *	Rationalizing a bit the interface of Hints.	Pierre-Marie Pédrot	2015-05-11
\| *	Fix bug #4212, congruence forgetting about some universe constraints.	Matthieu Sozeau	2015-05-05
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|\\|
* \|	maintenance micromega plugin	Frédéric Besson	2015-04-28
\| *	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
\| *	Using tclZEROMSG instead of tclZERO in several places.	Pierre-Marie Pédrot	2015-04-23
\| *	Declarative mode: remaining goals are "given up" when closing blocks.	Arnaud Spiwack	2015-04-22
\| *	Remove dirty debug printing from funind.	Maxime Dénès	2015-04-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-04-15
\|\\|
\| *	Function now supports puniveres	jforest	2015-04-14
\| *	better debug in recdef	jforest	2015-04-14
\| *	Opaque implementation of auto tactics.	Pierre-Marie Pédrot	2015-04-14
\| *	correction of a bug reported by Tristan Crolard	jforest	2015-04-13
\| *	Fixing bug #4186.	Pierre-Marie Pédrot	2015-04-13
\| *	Fix #3590 for good this time, by changing the API, change's argument now	Matthieu Sozeau	2015-04-10