coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond	2016-01-05
\|\
\| *	Put implicits back as in 8.4.	Matthieu Sozeau	2015-12-31
\| *	Fix bug #4456, anomaly in handle-side effects	Matthieu Sozeau	2015-12-31
* \|	Merge branch 'v8.5' into trunk	Guillaume Melquiond	2015-12-31
\|\\|
* \|	External tactics and notations now accept any tactic argument.	Pierre-Marie Pédrot	2015-12-30
\| *	Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found.	Pierre-Marie Pédrot	2015-12-29
* \|	Fixing a bug in the order of side conditions for introduction pattern -> and <-.	Hugo Herbelin	2015-12-25
* \|	Fixing an "injection as" bug in the presence of side conditions.	Hugo Herbelin	2015-12-25
\| *	Inclusion of functors with restricted signature is now forbidden (fix #3746)	Pierre Letouzey	2015-12-22
\| *	(Partial) fix for bug #4453: raise an error instead of an anomaly.	Matthieu Sozeau	2015-12-17
* \|	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