coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6522: Fix core hint database issue #6521	Maxime Dénès	2018-03-08
\|\
* \	Merge PR #6816: Adding mention of shelved/given-up status in Show Existentials	Maxime Dénès	2018-03-08
\|\ \
* \ \	Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...	Maxime Dénès	2018-03-08
\|\ \ \
* \ \ \	Merge PR #6899: [compat] Remove "Standard Proposition Elimination"	Maxime Dénès	2018-03-08
\|\ \ \ \
* \ \ \ \	Merge PR #6582: Mangle auto-generated names	Maxime Dénès	2018-03-08
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6903: [compat] Remove "Shrink Abstract"	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 #6790: Allow universe declarations for [with Definition].	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
\|\ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| * \| \|	An experimental 'Show Extraction' command (grant feature wish #4129)	Pierre Letouzey	2018-03-06
\| \| \| \| \| * \| \| \| \| \|	[compat] Remove "Shrink Abstract"	Emilio Jesus Gallego Arias	2018-03-06
\| \|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ...	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \|	CHANGES and tests for with Definition @{univs}	Gaëtan Gilbert	2018-03-05
\| \| \| \| * \| \| \| \| \| \| \|	Sanitize universe declaration in Context (stop using a ref...)	Gaëtan Gilbert	2018-03-05
\| \| \| \| \|/ / / / / / /
* \| \| \| \| \| \| \| \| \| \|	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \| \| \| \|	[compat] Remove NOOP and alias deprecated options.	Emilio Jesus Gallego Arias	2018-03-04
\| \| \| \| \|/ / / / / / / \| \| \| \|/\| \| \| \| \| \| \|
\| \| * / \| \| \| \| \| \| \|	Remove deprecated options related to typeclasses.	Théo Zimmermann	2018-03-04
\| \| \|/ / / / / / / /
\| \| \| \| * / / / / /	ssr: add Prenex Implicits for Some_inj to use it as a view	Anton Trunov	2018-03-04
\| \| \| \|/ / / / / / \| \| \|/\| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #935: Handling evars in the VM	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \| \|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #6791: Removing compatibility support for versions older than 8.5.	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ...	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #915: Fix rewrite in * side conditions	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \| \| \|	Removing test for bug #2850.	Pierre-Marie Pédrot	2018-03-03
\| \| \| \| * \| \| \| \| \| \| \|	Adding a test file for evar handling in the VM.	Pierre-Marie Pédrot	2018-03-03
\| \| \| \| \| \|_\|_\|_\|/ / / \| \| \| \| \|/\| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \|	[compat] Remove "Standard Proposition Elimination"	Emilio Jesus Gallego Arias	2018-03-03
\| \| \| \| \| \|_\|_\|/ / / \| \| \| \| \|/\| \| \| \| \|
\| \| \| * \| \| \| \| \| \|	Remove 8.5 compatibility support.	Théo Zimmermann	2018-03-02
\| \| \| * \| \| \| \| \| \|	Remove VOld compatibility flag.	Théo Zimmermann	2018-03-02
\| \| \| * \| \| \| \| \| \|	Turn warning for deprecated notations on.	Théo Zimmermann	2018-03-02
\| \| \| \|/ / / / / /
\| \| * / / / / / /	Fix #6878: univ undefined for [with Definition] bad instance size.	Gaëtan Gilbert	2018-03-01
\| \| \|/ / / / / /
\| * / / / / / /	Fixing rewriting in side conditions for "rewrite in " and "rewrite in \|-".	Hugo Herbelin	2018-03-01
\| \|/ / / / / /
* / / / / / /	[test-suite] Add a basic test-case for `Load`.	Emilio Jesus Gallego Arias	2018-02-28
\|/ / / / / /
* \| \| \| \| \|	Merge PR #6756: Fix issue with spurious timing test failures	Maxime Dénès	2018-02-28
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinit...	Maxime Dénès	2018-02-28
\|\ \ \ \ \ \ \
\| \| \| * \| \| \| \|	Update headers following #6543.	Théo Zimmermann	2018-02-27
\| \|_\|/ / / / / \|/\| \| \| \| \| \|
\| \| * \| \| \| \|	[test-suite] Move sed scripts into bash arrays	Jason Gross	2018-02-24
* \| \| \| \| \| \|	Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).	Maxime Dénès	2018-02-24
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6599: Decimals in prelude	Maxime Dénès	2018-02-24
\|\ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \|	Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).	Hugo Herbelin	2018-02-23
\| \|_\|/ / / / / / \|/\| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	Adding mention of shelved/given-up status in "Show Existentials".	Hugo Herbelin	2018-02-22
\| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`	Maxime Dénès	2018-02-21
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)	Maxime Dénès	2018-02-21
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just the...	Maxime Dénès	2018-02-21
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6740: Adding a sanity check on inductive variance subtyping.	Maxime Dénès	2018-02-21
\|\ \ \ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \| \| \|	Update SearchPattern.out for numeral notations	Jason Gross	2018-02-20
\| \|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \|	Fixes bug #6774 (anomaly with ill-typed template polymorphism).	Hugo Herbelin	2018-02-20
\| \|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \|	Adding a test for wish #5532.	Hugo Herbelin	2018-02-20