coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
* \|	Merge branch 'v8.5' into trunk	Pierre Letouzey	2015-04-09
\|\\|
\| *	JSON extraction: make explicit each group of mutually-recursive fixpoints	Nickolai Zeldovich	2015-04-09
\| *	JSON extraction: construct full names (dot-separated) in pp_global	Nickolai Zeldovich	2015-04-09
\| *	Add extraction to JSON.	Nickolai Zeldovich	2015-04-09
\| *	add ExtrHaskellBasic.v to mirror ExtrOcamlBasic.v	Nickolai Zeldovich	2015-04-08
\| *	Fix specialized extraction of ascii characters into Haskell. (Fix bug #4181)	Nickolai Zeldovich	2015-04-08
\| *	Puts all the "import" statements first so as to accommodate the latest GHC.	Nickolai Zeldovich	2015-04-02
\| *	Fix some typos.	Guillaume Melquiond	2015-04-02
\| *	Define Any in Haskell extraction when Tunknown is used.	Nickolai Zeldovich	2015-04-02
\| *	Accomodating #4166 (providing "Require Import OmegaTactic" as a	Hugo Herbelin	2015-04-01
\| *	Declarative mode: fix proof modes.	Arnaud Spiwack	2015-03-31
\| *	Declarative mode: fix vernac classification.	Arnaud Spiwack	2015-03-31
\| *	Declarative mode: plug the specialised printers back.	Arnaud Spiwack	2015-03-31
* \|	Merge branch 'v8.5' into trunk	Enrico Tassi	2015-03-30
\|\\|
\| *	Correcting a bug introduced by universes polymorphism	jforest	2015-03-25
\| *	correcting a bug with aliased when using Functional Scheme	forest	2015-03-25
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-23
\|\\|
\| *	Avoid segfault from code extracted to ghc. (Fix for bug #1257)	Guillaume Melquiond	2015-03-21
\| *	Properly capitalize filenames when extracting to Haskell. (Fix for bug #3221)	Guillaume Melquiond	2015-03-21
\| *	Do not revert parameter lists when extracting singleton types to Haskell. (Fi...	Guillaume Melquiond	2015-03-21
* \|	Merge branch 'v8.5' into trunk	Arnaud Spiwack	2015-03-13
\|\\|
\| *	Declarative mode: make it so that unfocussing can only be done for closed sub...	Arnaud Spiwack	2015-03-13
\| *	Declarative mode: remove dead code.	Arnaud Spiwack	2015-03-13
\| *	Declarative mode: remove a superfluous [set_proof_mode].	Arnaud Spiwack	2015-03-13
\| *	Declarative mode: fix the focus behaviour.	Arnaud Spiwack	2015-03-13
\| *	rewiring Czar printers that were disabled	Pierre Corbineau	2015-03-13
\| *	Fix double print in decl_mode.	Enrico Tassi	2015-03-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-11
\|\\|
\| *	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi	2015-03-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-04
\|\\|
\| *	Fix bug #3732: firstorder was using detyping to build existential	Matthieu Sozeau	2015-03-03