coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-09
\|\
\| *	Fix test-suite file coq-prog-args	Matthieu Sozeau	2016-03-09
\| *	Fixed bug #4533 with previous Keyed Unification commit	Matthieu Sozeau	2016-03-09
\| *	Fix strategy of Keyed Unification	Matthieu Sozeau	2016-03-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\\|
* \|	Using build_selector from Equality as a replacement of the selector	Hugo Herbelin	2016-03-05
* \|	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
\| *	Adding a test for the behaviour of open_constr described in #3777.	Pierre-Marie Pédrot	2016-03-03
* \|	Moving the "clear" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
\| *	Fixing bug #4596: [rewrite] broke in the past few weeks.	Pierre-Marie Pédrot	2016-02-28
\| *	Document differences of Hint Resolve and Hint Extern	Matthieu Sozeau	2016-02-23
* \|	Moving the Tauto tactic to proper Ltac.	Pierre-Marie Pédrot	2016-02-22
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-21
\|\\|
\| *	Fixing bug #4580: [Set Refine Instance Mode] also used for Program Instance.	Pierre-Marie Pédrot	2016-02-19
\| *	Fixing bug #4582: cannot override notation [ x ].	Pierre-Marie Pédrot	2016-02-19
\| *	STM: Print/Extraction have to be skipped if -quick	Enrico Tassi	2016-02-19
\| *	Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").	Pierre-Marie Pédrot	2016-02-17
* \|	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