coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ...	Maxime Dénès	2017-11-30
\|\
\| *	In injection/inversion, consider all template-polymorphic types as injectable.	Hugo Herbelin	2017-11-28
* \|	Fix (partial) #4878: option to stop autodeclaring axiom as instance.	Gaëtan Gilbert	2017-11-28
* \|	Fix #5347: unify declaration of axioms with and without bound univs.	Gaëtan Gilbert	2017-11-25
* \|	Make restrict_universe_context stronger.	Gaëtan Gilbert	2017-11-25
\|/
*	Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRing	Maxime Dénès	2017-11-24
\|\
* \	Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion	Maxime Dénès	2017-11-24
\|\ \
* \ \	Merge PR #6203: Fix universe polymorphic Program obligations.	Maxime Dénès	2017-11-23
\|\ \ \
\| \| * \|	Recognizing Z in romega up to conversion.	Hugo Herbelin	2017-11-23
\| \| * \|	Using is_conv rather than eq_constr to find `nat` or `Z` in omega.	Hugo Herbelin	2017-11-23
\| \|/ / \|/\| \|
\| \| *	Fixing a 8.7 regression of ring_simplify in ArithRing.	Hugo Herbelin	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
\|\ \ \