coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6178: Have the coq_makefile timing test-suite print more	Maxime Dénès	2017-11-21
\|\
* \	Merge PR #6113: Extra work on ltac printing: fixing #5787, some parentheses	Maxime Dénès	2017-11-21
\|\ \
\| * \|	Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).	Hugo Herbelin	2017-11-20
* \| \|	Merge PR #6166: Fix regression in treating Defined as defined	Maxime Dénès	2017-11-20
\|\ \ \
* \ \ \	Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause...	Maxime Dénès	2017-11-20
\|\ \ \ \
* \ \ \ \	Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces unbo...	Maxime Dénès	2017-11-20
\|\ \ \ \ \
\| \| \| \| \| *	Have the coq_makefile timing test-suite print more	Jason Gross	2017-11-17
\| \|_\|_\|_\|/ \|/\| \| \| \|
* \| \| \| \|	Merge PR #6132: Fixes #6129 (declaration of coercions made compatible with lo...	Maxime Dénès	2017-11-16
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6104: Fixing encoding in coqdoc output tests.	Maxime Dénès	2017-11-16
\|\ \ \ \ \ \ \| \|_\|_\|_\|_\|/ \|/\| \| \| \| \|
\| \| \| \| \| *	Fix regression in treating Defined as defined	Tej Chajed	2017-11-15
\| \|_\|_\|_\|/ \|/\| \| \| \|
\| \| \| * \|	Fix #5761: cbv on undefined evars under binders produces unbound rel	Gaëtan Gilbert	2017-11-15
\| \|_\|/ / \|/\| \| \|
* \| \| \|	Merge PR #6122: Remove dependency of test-suite on git (fix #5725).	Maxime Dénès	2017-11-15
\|\ \ \ \
\| \| \| * \|	Fixes #6129 (declaration of coercions made compatible with local definitions).	Hugo Herbelin	2017-11-14
\| \|_\|/ / \|/\| \| \|
\| \| \| *	One more step in fixing #5762 ("where" clause).	Hugo Herbelin	2017-11-14
\| \| * \|	Fixing encoding in coqdoc output tests.	Hugo Herbelin	2017-11-13
* \| \| \|	Merge PR #6000: Adding support for syntax "let _ := e in e'" in Ltac.	Maxime Dénès	2017-11-13
\|\ \ \ \
\| \| \| \| *	Fixing a remaining "coqdoc" problem with bug #5762 and pr #1120.	Hugo Herbelin	2017-11-08
\| \| \| \|/
\| \| * /	Remove dependency of test-suite on git (fix #5725).	Théo Zimmermann	2017-11-08
\| \|/ / \|/\| \|
* \| \|	Merge PR #922: New beta-iota compatibility refinements	Maxime Dénès	2017-11-08
\|\ \ \ \| \|_\|/ \|/\| \|
* \| \|	Merge PR #6074: Refining PR#924 (insensitivity of projection heuristics to al...	Maxime Dénès	2017-11-06
\|\ \ \
* \ \ \	Merge PR #1139: Add a linter.	Maxime Dénès	2017-11-06
\|\ \ \ \
\| \| * \| \|	Refining PR#924 (insensitivity of projection heuristics to alphabet).	Hugo Herbelin	2017-11-05
\| \|/ / / \|/\| \| \|
\| \| \| *	Adding support for syntax "let _ := e in e'" in Ltac.	Hugo Herbelin	2017-11-04
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #6047: A generic printer for ltac values	Maxime Dénès	2017-11-03
\|\ \ \
* \ \ \	Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous varia...	Maxime Dénès	2017-11-03
\|\ \ \ \
* \ \ \ \	Merge PR #6021: Fixing #2881 ("change with" failing in an Ltac definition).	Maxime Dénès	2017-11-03
\|\ \ \ \ \
\| \| \| * \| \|	Binding ltac printing functions to the system of generic printing.	Hugo Herbelin	2017-11-02
\| \|_\|/ / / \|/\| \| \| \|
\| * \| \| \|	Fixing #2881 ("change with" failing in an Ltac definition).	Hugo Herbelin	2017-10-30
\| \| * \| \|	Fixing #5401 (printing of patterns with bound anonymous variables).	Hugo Herbelin	2017-10-28
\| \|/ / / \|/\| \| \|
* \| \| \|	Merge PR #677: Trunk+abstracting injection flags	Maxime Dénès	2017-10-27
\|\ \ \ \ \| \|/ / / \|/\| \| \|
\| * \| \|	Passing around the flag for injection so that tactics calling inj at	Hugo Herbelin	2017-10-26
\| \| * \|	Put newlines at the end of files.	Gaëtan Gilbert	2017-10-25
* \| \| \|	Move bug files to match their new GitHub ID (fixes #6001).	Théo Zimmermann	2017-10-23
\|/ / /
* \| \|	Merge PR #5989: Handle ∞ in coq-makefile timing test-suite	Maxime Dénès	2017-10-20
\|\ \ \
* \ \ \	Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...	Maxime Dénès	2017-10-20
\|\ \ \ \
\| \| * \| \|	Handle ∞ in coq-makefile timing test-suite	Jason Gross	2017-10-19
* \| \| \| \|	Moving bug numbers to BZ# format in the test-suite.	Théo Zimmermann	2017-10-19
\| \|/ / / \|/\| \| \|
* \| \| \|	Adding a test for bug BZ#5692.	Pierre-Marie Pédrot	2017-10-17
* \| \| \|	[stdlib] Fix warnings on deprecated `Add Setoid`	Emilio Jesus Gallego Arias	2017-10-15
* \| \| \|	Use a nice printer for constant names in Suggest Proof Using.	Gaëtan Gilbert	2017-10-10
* \| \| \|	Take Suggest Proof Using outside the kernel.	Gaëtan Gilbert	2017-10-10
* \| \| \|	Merge PR #768: Omega and romega know about context definitions (fix old bug 148)	Maxime Dénès	2017-10-10
\|\ \ \ \
* \ \ \ \	Merge PR #1126: [ltac] Warning for deprecated `Add Setoid` and `Add Morphism`...	Maxime Dénès	2017-10-09
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-on...	Maxime Dénès	2017-10-09
\|\ \ \ \ \ \ \| \|_\|_\|_\|/ / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type "_som...	Maxime Dénès	2017-10-06
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #1121: Fixing BZ#5765 (an anomaly with 'pat in the parameters of an ...	Maxime Dénès	2017-10-06
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #1124: Extraction: reduce atomic eta-redexes (solves indirectly BZ#4...	Maxime Dénès	2017-10-06
\|\ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \|	[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.	Emilio Jesus Gallego Arias	2017-10-05
\| \|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \|
\| \| \| \| \| * \| \|	romega: takes advantage of context variables with body	Pierre Letouzey	2017-10-05
\| \| \| \| \| * \| \|	Omega now aware of context variables with bodies (in type Z or nat) (fix bug ...	Pierre Letouzey	2017-10-05
\| \|_\|_\|_\|/ / / \|/\| \| \| \| \| \|