coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6203: Fix universe polymorphic Program obligations.	Maxime Dénès	2017-11-23
\|\
* \	Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag.	Maxime Dénès	2017-11-23
\|\ \
\| \| *	Fix universe polymorphic Program obligations.	Matthieu Sozeau	2017-11-22
\| \|/ \|/\|
* \|	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
\|\ \ \ \
\| \| \| \| *	Fix #5790: make Hint Resolve <- respect univ polymorphism flag.	Gaëtan Gilbert	2017-11-19
\| \|_\|_\|/ \|/\| \| \|
\| \| \| *	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
\| \| \|/ \| \|/\|
* / \|	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
* \|	Merge PR #6000: Adding support for syntax "let _ := e in e'" in Ltac.	Maxime Dénès	2017-11-13
\|\ \ \| \|/ \|/\|
* \|	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 #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...	Maxime Dénès	2017-10-20
\|\ \
* \| \|	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
* \| \|	Merge PR #768: Omega and romega know about context definitions (fix old bug 148)	Maxime Dénès	2017-10-10
\|\ \ \ \| \|_\|/ \|/\| \|
* \| \|	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
\|\ \ \ \ \
\| \| \| \| * \|	Omega now aware of context variables with bodies (in type Z or nat) (fix bug ...	Pierre Letouzey	2017-10-05
\| \|_\|_\|/ / \|/\| \| \| \|
* \| \| \| \|	Merge PR #1102: On the detection of evars which "advanced" (and a fix to BZ#5...	Maxime Dénès	2017-10-05
\|\ \ \ \ \
\| \| * \| \| \|	Extraction: reduce eta-redexes whose cores are atomic (solves indirectly BZ#4...	Pierre Letouzey	2017-10-05
\| \|/ / / / \|/\| \| \| \|
\| \| \| * \|	Fixing BZ#5769 (variable of type "_something" was named after invalid "_").	Hugo Herbelin	2017-10-05
\| \| * \| \|	Fixing #5765 (an anomaly with 'pat in parameters of inductive definition).	Hugo Herbelin	2017-10-05
\| \| \|/ /
\| \| \| *	Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).	Hugo Herbelin	2017-10-05
\| \| \|/
* \| \|	Merge PR #1006: fix: ssrmatching and primitive projections	Maxime Dénès	2017-10-04
\|\ \ \
* \ \ \	Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial).	Maxime Dénès	2017-10-04
\|\ \ \ \ \| \|_\|_\|/ \|/\| \| \|
\| \| \| *	Moving setting of "cleared" evar flag directly in Evd.restrict.	Hugo Herbelin	2017-09-27
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ...	Maxime Dénès	2017-09-25
\|\ \ \
* \ \ \	Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in 4...	Maxime Dénès	2017-09-25
\|\ \ \ \
\| \| * \| \|	Fixing #5755 (discharging of inductive types not correct with let-ins).	Hugo Herbelin	2017-09-23
\| \|/ / / \|/\| \| \|
\| * \| \|	Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).	Hugo Herbelin	2017-09-23
* \| \| \|	A possible fix to BZ#5750 (ability to print context of ltac subterm match).	Hugo Herbelin	2017-09-21
\|/ / /
\| \| *	ssr: fix canonical strucut key comparison with primproj on	Enrico Tassi	2017-09-20
\| * \|	Fixing bug #5741 (anomaly in info_trivial).	Hugo Herbelin	2017-09-19
\|/ /
* \|	Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).	Maxime Dénès	2017-09-19
\|\ \ \| \|/ \|/\|