coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-13
\|\
\| *	Do not give a name to anonymous evars anymore. See bug #4547.	Pierre-Marie Pédrot	2016-02-13
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\\|
\| *	Adding a test for bug #4378.	Pierre-Marie Pédrot	2016-01-24
\| *	Fixing bug #4495: Failed assertion in metasyntax.ml.	Pierre-Marie Pédrot	2016-01-24
\| *	Fixing bug #4511: evar tactic can create non-typed evars.	Pierre-Marie Pédrot	2016-01-24
\| *	Fix bug #4503: mixing universe polymorphic and monomorphic	Matthieu Sozeau	2016-01-23
\| *	Fix bug #4519: oops, global shadowed local universe level bindings.	Matthieu Sozeau	2016-01-23
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
* \|	Stronger invariants on the use of the introduction pattern (pat1,...,patn).	Hugo Herbelin	2016-01-21
* \|	Fixing some problems with double induction.	Hugo Herbelin	2016-01-21
* \|	Fixing a bug with introduction patterns over inductive types containing let-ins.	Hugo Herbelin	2016-02-18
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
\| *	Fix bug #4420: check_types was losing universe constraints.	Matthieu Sozeau	2016-01-19
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-13
\|\\|
\| *	Fixing success of test for #3848 after move to directory "closed".	Hugo Herbelin	2016-01-13
\| *	Fixing #4467 (continued).	Hugo Herbelin	2016-01-13
\| *	Fixing #4467 (missing shadowing of variables in cases pattern).	Hugo Herbelin	2016-01-12
\| *	Fixing #4256 and #4484 (changes in evar-evar resolution made that new	Hugo Herbelin	2016-01-12
\| *	Extend last commit: keyed unification uses full conversions on the applied co...	Matthieu Sozeau	2016-01-12
\| *	Extend Keyed Unification tests with the one from R. Krebbers.	Matthieu Sozeau	2016-01-12
* \|	Fix bug 4479: "Error: Rewriting base foo does not exist." should be catchable.	Pierre-Marie Pédrot	2016-01-09
\| *	Fix bug #4480: progress was not checked for setoid_rewrite.	Matthieu Sozeau	2016-01-07
* \|	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
\|\\|