coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-17
\|\
\| *	Proof using: do not clear unused section hyps automatically	Enrico Tassi	2015-12-15
\| *	Fix test suite after change in extraction.	Maxime Dénès	2015-12-15
\| *	Extraction: more cautious use of intermediate result caching (fix #3923)	Pierre Letouzey	2015-12-15
\| *	Fix test-suite files after change in refine tactic.	Maxime Dénès	2015-12-15
\| *	Adding a test for the unshelve tactical.	Pierre-Marie Pédrot	2015-12-15
\| *	Refine tactic now shelves unifiable holes.	Pierre-Marie Pédrot	2015-12-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-15
\|\\|
\| *	extraction_impl.v: fix a typo	Pierre Letouzey	2015-12-14
\| *	A test file for Extraction Implicit (including bugs #4243 and #4228)	Pierre Letouzey	2015-12-14
\| *	Test file for #4363 was not complete.	Maxime Dénès	2015-12-14
\| *	Univs: Fix bug #4363, nested abstract.	Matthieu Sozeau	2015-12-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\\|
\| *	Fixing a pat%constr bug. Thanks to Enrico for reporting.	Hugo Herbelin	2015-12-10
\| *	Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.	Hugo Herbelin	2015-12-10
\| *	bug fixes to vm computation + test cases.	Gregory Malecha	2015-12-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-08
\|\\|
\| *	Fix some typos.	Guillaume Melquiond	2015-12-07
* \|	Using x in output test-suite Cases.v (cosmetic).	Hugo Herbelin	2015-12-05
\| *	Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)	Hugo Herbelin	2015-12-05
\| *	Univs: fix bug #4443.	Matthieu Sozeau	2015-12-03
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\\|
\| *	Adding a target report to test-suite's Makefile to get a short summary.	Hugo Herbelin	2015-12-02
\| *	Improving syntax of pat/constr introduction pattern so that	Hugo Herbelin	2015-12-02
\| *	Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.	Hugo Herbelin	2015-12-02
* \|	New algorithm for universe cycle detections.	Jacques-Henri Jourdan	2015-12-01
\| *	Test for bug #4149.	Pierre-Marie Pédrot	2015-11-30
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|
\| *	Test-suite files for closed bugs	Matthieu Sozeau	2015-11-28
\| *	Closed bugs.	Matthieu Sozeau	2015-11-28
\| *	Univs: entirely disallow instantiation of polymorphic constants with	Matthieu Sozeau	2015-11-27
\| *	Fixing the "parsing rules with idents later declared as keywords" problem.	Hugo Herbelin	2015-11-26
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-26
\|\\|
\| *	Fixing a vm_compute bug in the presence of let-ins among the	Hugo Herbelin	2015-11-22
\| *	Fixing a bug of adjust_subst_to_rel_context.	Hugo Herbelin	2015-11-22
\| *	Fixing kernel bug in typing match with let-ins in the arity.	Hugo Herbelin	2015-11-22
* \|	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
\| *	Fixing logical bugs in the presence of let-ins in computiong primitive	Hugo Herbelin	2015-11-18
* \|	Fixing output test Cases.v.	Pierre-Marie Pédrot	2015-11-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-15
\|\\|
\| *	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
\| *	Now closed.	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
* \|	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