coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing #7700 (section variables bound to abbreviations were not found).	Hugo Herbelin	2018-06-10
*	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
\| \| \| \| \|/ \| \| \| \|/\|
* \| \| / \|	Fix #6956: Uncaught exception in bytecode compilation	Maxime Dénès	2018-04-06
\| \|_\|/ / \|/\| \| \|
\| * \| \|	Fix #5981, bugs/opened/3263.v is non-deterministic by removing the test.	Théo Zimmermann	2018-04-05
\|/ / /
* \| \|	Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)	Pierre-Marie Pédrot	2018-04-01
\|\ \ \
* \| \| \|	Change Implicit Arguments to Arguments in test-suite	Jasper Hugunin	2018-03-30
\| \| \| *	Fix #6770: fixpoint loses locality info in proof mode.	Gaëtan Gilbert	2018-03-29
* \| \| \|	Fix #6631: Derive Plugin gives "Anomaly: more than one statement".	Pierre-Marie Pédrot	2018-03-29
\| \|_\|/ \|/\| \|
\| * \|	Supporting fix/cofix in Ltac pattern-matching (wish #7092).	Hugo Herbelin	2018-03-28
\|/ /
\| *	Fixes #7011 (Fix/CoFix were not considered in tactic unification).	Hugo Herbelin	2018-03-26
\|/
*	Allow using cumulativity without forcing strict constraints.	Gaëtan Gilbert	2018-03-09
*	Merge PR #6895: [compat] Remove "Refolding Reduction" option.	Maxime Dénès	2018-03-09
\|\
* \|	More examples about shelve/given_up in tactic-in-terms.	Hugo Herbelin	2018-03-08
* \|	Proof engine: support for nesting tactic-in-term within other tactics.	Hugo Herbelin	2018-03-08
\| *	[compat] Remove "Refolding Reduction" option.	Emilio Jesus Gallego Arias	2018-03-08
\|/
*	Merge PR #6899: [compat] Remove "Standard Proposition Elimination"	Maxime Dénès	2018-03-08
\|\
* \	Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)	Maxime Dénès	2018-03-08
\|\ \
* \ \	Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`	Maxime Dénès	2018-03-07
\|\ \ \
* \ \ \	Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)	Maxime Dénès	2018-03-07
\|\ \ \ \
\| \| \| * \|	ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)	Enrico Tassi	2018-03-06
* \| \| \| \|	Merge PR #6896: [compat] Remove NOOP deprecated options.	Maxime Dénès	2018-03-06
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6824: Remove deprecated options related to typeclasses.	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \ \| \|_\|_\|_\|/ / \|/\| \| \| \| \|
\| \| \| * \| \|	Sanitize universe declaration in Context (stop using a ref...)	Gaëtan Gilbert	2018-03-05