coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \|	Moving the parsing of the Ltac proof mode to G_ltac.	Pierre-Marie Pédrot	2016-03-19
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-18
\|\ \ \
\| \| * \|	Fix bug #4627: records with no declared arity can be template polymorphic.	Matthieu Sozeau	2016-03-17
\| \| * \|	Test file for #4623.	Maxime Dénès	2016-03-17
\| \| * \|	Test file for #4624, fixed by Matthieu's bfce815bd1.	Maxime Dénès	2016-03-16
\| \|/ /
\| * \|	According to Bruno, my fix for #4588 seems to be enough.	Maxime Dénès	2016-03-11
* \| \|	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
\|\\| \|
* \| \|	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
* \| \|	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
* \| \|	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
\| * \|	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
\|\\| \|
\| * \|	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 (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
* \| \|	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
\| * \|	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
\|\\| \|
\| * \|	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
\| * \|	Refine tactic now shelves unifiable holes.	Pierre-Marie Pédrot	2015-12-15
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-15
\|\\| \|
\| * \|	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