coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-20
\|\
\| *	Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.	Pierre-Marie Pédrot	2015-11-19
\| *	Allow program hooks to see the refined universe_context at the end of a	Matthieu Sozeau	2015-11-19
\| *	Fix bug #4433, removing hack on evars appearing in a pattern from a	Matthieu Sozeau	2015-11-19
\| *	Fixing fix c71aa6b to primitive projections.	Hugo Herbelin	2015-11-18
\| *	Fix a bug preventing the generation of graphs when doing multiple	Matthieu Sozeau	2015-11-18
\| *	Improve error message.	Maxime Dénès	2015-11-18
\| *	MacOS package script: do not fail if link to /Applications already exists.	Maxime Dénès	2015-11-18
\| *	Slightly documenting code for building primitive projections.	Hugo Herbelin	2015-11-18
\| *	Fixing logical bugs in the presence of let-ins in computiong primitive	Hugo Herbelin	2015-11-18
* \|	Inlining the only use of Clenv.connect_clenv.	Pierre-Marie Pédrot	2015-11-18
\| *	More optimizations of [Clenv.clenv_fchain].	Pierre-Marie Pédrot	2015-11-17
\| *	Performance fix for destruct.	Pierre-Marie Pédrot	2015-11-17
\| *	Being more precise and faithful about the origin of the file reporting	Hugo Herbelin	2015-11-16
* \|	Hashconsing modules.	Pierre-Marie Pédrot	2015-11-15
* \|	Fixing output test Cases.v.	Pierre-Marie Pédrot	2015-11-15
* \|	Displaying the object identifier in votour.	Pierre-Marie Pédrot	2015-11-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-15
\|\\|
\| *	Continue fix of PMP, handling setoid_rewrite in let-bound hyps correctly.	Matthieu Sozeau	2015-11-13
\| *	MacOS package script: do not fail if directory _dmg already exists.	Maxime Dénès	2015-11-13
\| *	Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.	Pierre-Marie Pédrot	2015-11-12
\| *	Fixed test-suite file for bug #3998.	Matthieu Sozeau	2015-11-12
\| *	Update CHANGES	Jason Gross	2015-11-12
\| *	Script building MacOS package.	Maxime Dénès	2015-11-12
\| *	Now closed.	Matthieu Sozeau	2015-11-11
\| *	Ensure that conversion is called on terms of the same type in	Matthieu Sozeau	2015-11-11
\| *	Fix bug #3998: when using typeclass resolution for conversion, allow	Matthieu Sozeau	2015-11-11
\| *	Fix bug #3735: interpretation of "->" in Program follows the standard one.	Matthieu Sozeau	2015-11-11
\| *	Fix bug #3257, setoid_reflexivity should fail if not completing the goal.	Matthieu Sozeau	2015-11-11
\| *	Fix bug #4293: ensure let-ins do not contain algebraic universes in	Matthieu Sozeau	2015-11-11
\| *	Fixing bug #3554: Anomaly: Anonymous implicit argument.	Pierre-Marie Pédrot	2015-11-11
* \|	Updating test-suite after Bracketing Last Introduction Pattern set by	Hugo Herbelin	2015-11-10
* \|	Updating Compat85.v after bd1c97653 on bracketing last or-and	Hugo Herbelin	2015-11-10
* \|	Revert "Fixing #1225: we now skip the canonically built binding contexts of"	Hugo Herbelin	2015-11-10
* \|	Fixing #1225: we now skip the canonically built binding contexts of	Hugo Herbelin	2015-11-10
* \|	Listing separately changes from 8.5betas to final 8.5 and further	Hugo Herbelin	2015-11-10
* \|	Activating bracketing of last or-and introduction pattern by default	Hugo Herbelin	2015-11-10
* \|	Merge origin/v8.5 into trunk	Hugo Herbelin	2015-11-10
\|\\|
\| *	Dead code from the commit having introduced primitive projections (a4043608).	Hugo Herbelin	2015-11-10
\| *	Typo.	Hugo Herbelin	2015-11-10
\| *	Fixing a bug in reporting ill-formed constructor.	Hugo Herbelin	2015-11-10
\| *	Test for bug #4404.	Pierre-Marie Pédrot	2015-11-10
\| *	Fix bug #4404: [remember] gives Error: Conversion test raised an anomaly.	Pierre-Marie Pédrot	2015-11-10
\| *	Pushing the backtrace in conversion anomalies.	Pierre-Marie Pédrot	2015-11-09
* \|	Adapting output test inference.v after c23f0cab6 (experimenting	Hugo Herbelin	2015-11-08
\| *	Fixing output test Existentials.v after eec77191b.	Hugo Herbelin	2015-11-07
* \|	Preventing an unwanted warning 5 "this function application is partial"	Hugo Herbelin	2015-11-07
* \|	Implementing assert and cut with LetIn rather than using a beta-redex.	Hugo Herbelin	2015-11-07
* \|	Experimenting printing the type of the defined term of a LetIn when	Hugo Herbelin	2015-11-07
* \|	Adding an amazing property of Prop.	Hugo Herbelin	2015-11-07