coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Correct some spelling errorsmaster	Benjamin Barenblat	2018-07-22
*	Merge PR #7884: Fix #5719: Uncaught exception Invalid_argument.	Matthieu Sozeau	2018-07-09
\|\
* \|	Add test for #8004.	Gaëtan Gilbert	2018-07-06
* \|	Fixes #7712 (an anomaly in reporting bad recursive notation format).	Hugo Herbelin	2018-06-29
* \|	Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)	Pierre-Marie Pédrot	2018-06-27
\|\ \
\| * \|	Test file for #7723	Maxime Dénès	2018-06-27
* \| \|	Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations).	Hugo Herbelin	2018-06-26
\|/ /
* \|	Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...	Matthieu Sozeau	2018-06-25
\|\ \
* \ \	Merge PR #7559: Existing Class noop when already a class + warning.	Matthieu Sozeau	2018-06-25
\|\ \ \
\| \| * \|	Remove hack skipping comparison of algebraic universes in subtyping.	Gaëtan Gilbert	2018-06-22
\| \|/ / \|/\| \|
\| \| *	Fix #5719: Uncaught exception Invalid_argument.	Pierre-Marie Pédrot	2018-06-21
\| \|/ \|/\|
* \|	Fix #7421: constr_eq ignores universe constraints.	Gaëtan Gilbert	2018-06-18
* \|	Fixes #7811 (uncaught Not_found in notation printer related to "match").	Hugo Herbelin	2018-06-17
* \|	Merge PR #7616: Fix #7615: Functor inlining drops universe substitution.	Maxime Dénès	2018-06-17
\|\ \
* \| \|	Workaround to handle non-value arguments in tactics.	Cyprien Mangin	2018-06-14
* \| \|	Merge PR #664: Fixing #5500 (missing test in return clause of match leading t...	Matthieu Sozeau	2018-06-14
\|\ \ \
* \ \ \	Merge PR #7787: Fixes #7780: missing lift in expanding alias under a binder i...	Matthieu Sozeau	2018-06-14
\|\ \ \ \
* \| \| \| \|	Fixes #7779 (destruct's "in" clause was forgetting the possibility of "eqn").	Hugo Herbelin	2018-06-12
\| * \| \| \|	Fixes #7780 (missing lift in expanding alias under a binder in unification).	Hugo Herbelin	2018-06-12
\|/ / / /
* \| \| \|	Fixing #7700 (section variables bound to abbreviations were not found).	Hugo Herbelin	2018-06-10
\| \| \| *	Existing Class noop when already a class + warning.	Gaëtan Gilbert	2018-06-08
\| \|_\|/ \|/\| \|
\| \| *	Fix #7615: Functor inlining drops universe substitution.	Pierre-Marie Pédrot	2018-06-07
\| \|/ \|/\|
* \|	Merge PR #7077: Preserving canonical structure of return predicate in vm_comp...	Maxime Dénès	2018-06-05
\|\ \
* \| \|	Fix #7631: native_compute fails to compile an example in Coq 8.8	Maxime Dénès	2018-06-04
\| * \|	Tests for part of #7068 and for #7076 (vm/native_compute and return predicate).	Hugo Herbelin	2018-06-04
\|/ /
* \|	Merge PR #7229: Deprecate implicit tactic solving.	Hugo Herbelin	2018-06-04
\|\ \
* \ \	Merge PR #7199: Fixes #7195: missing freshness condition in Ltac pattern-matc...	Matthieu Sozeau	2018-06-04
\|\ \ \
* \ \ \	Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.	Matthieu Sozeau	2018-06-04
\|\ \ \ \
* \ \ \ \	Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomaly	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7189: Fix #5539: algebraic universe produced by cases.	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ta...	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found".	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \|	Deprecate implicit tactic solving.	Pierre-Marie Pédrot	2018-06-04
\| \|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \|
* \| \| \| \| \| \| \|	Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel.	Maxime Dénès	2018-06-04
\|\ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \|	Fix #7113: Program Let Fixpoint in section causes anomaly	Gaëtan Gilbert	2018-05-30
* \| \| \| \| \| \| \| \|	Fix #6951: Unexpected error during scheme creation.	Pierre-Marie Pédrot	2018-05-29
\| \|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \|
* \| \| \| \| \| \| \|	Add test for #7333: vm_compute segfaults / Anomaly with cofix	Maxime Dénès	2018-05-29
\| \| * \| \| \| \| \|	Fix #7586: Anomaly "Uncaught exception Not_found".	Pierre-Marie Pédrot	2018-05-23
\| \|/ / / / / / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Add test cases from #7554	Tej Chajed	2018-05-20
* \| \| \| \| \| \|	Introduce an option to allow nested lemma, and turn it off by default.	Théo Zimmermann	2018-05-17
* \| \| \| \| \| \|	Merge PR #7479: Move 4722 (dangling symlink) to misc tests, remove dangling s...	Gaëtan Gilbert	2018-05-14
\|\ \ \ \ \ \ \
\| * \| \| \| \| \| \|	Move 4722 (dangling symlink) to misc tests, remove dangling symlink from repo	Ralf Jung	2018-05-13
\| \| * \| \| \| \| \|	Fix #4403: insufficient handling of type-in-type in kernel.	Gaëtan Gilbert	2018-05-13
\| \|/ / / / / /
* \| \| \| \| \| \|	Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).	Hugo Herbelin	2018-05-10
* \| \| \| \| \| \|	Fixes part 1 of #7462 (only-printing not to override existing interp rule).	Hugo Herbelin	2018-05-10
\|/ / / / / /
* \| \| \| \| \|	[ltac] Deprecate nameless fix/cofix.	Emilio Jesus Gallego Arias	2018-04-13
* \| \| \| \| \|	Merge PR #7179: Fix #5981, bugs/opened/3263.v is non-deterministic by removin...	Jason Gross	2018-04-12
\|\ \ \ \ \ \
* \| \| \| \| \| \|	Fix the status of some resolved bugs	Tej Chajed	2018-04-11
\| \| \| \| \| * \|	Fixes #7195 (missing freshness condition in Ltac pattern-matching names).	Hugo Herbelin	2018-04-08
\| \| \| * \| \| \|	Fix #5539: algebraic universe produced by cases.	Gaëtan Gilbert	2018-04-06
\| \| \| \| \|/ / \| \| \| \|/\| \|