coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6922: Remove outdated information regarding the FAQ.	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6374: [toplevel] Modify printing goal strategy.	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Add CHANGES and man entry for coqdep learning _CoqProject.	Gaëtan Gilbert	2018-03-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Closes #6830: coqdep reads options and files from _CoqProject.	Gaëtan Gilbert	2018-03-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	An experimental 'Show Extraction' command (grant feature wish #4129)	Pierre Letouzey	2018-03-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Extraction: switch to EConstr.t as the central type to extract from.	Pierre Letouzey	2018-03-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	romega: get rid of EConstr.Unsafe	Pierre Letouzey	2018-03-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|/ / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|/\| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	document -profile in dev/doc/setup.txt	Enrico Tassi	2018-03-06
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Standard headers for C and Python.	Maxime Dénès	2018-03-06
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[stdlib] Do not use deprecated notations	Vincent Laporte	2018-03-06
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Add some missing flushes in configure.	Maxime Dénès	2018-03-06
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	Hack to make bignum build on windows	Enrico Tassi	2018-03-06
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	build: win: turn off build/installation of gnu Make	Enrico Tassi	2018-03-06
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Clean-up remove always false useeager argument.	Théo Zimmermann	2018-03-06
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Remove outdated information regarding the FAQ.	Théo Zimmermann	2018-03-06
\| \|_\|_\|/ / / / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Rename some universe minimizing "normalize" functions to "minimize"	Gaëtan Gilbert	2018-03-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Deprecate UState aliases in Evd.	Gaëtan Gilbert	2018-03-06
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6917: Fix failing packaging job.	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	[compat] Remove "Discriminate Introduction"	Emilio Jesus Gallego Arias	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6900: [compat] Remove "Tactic Pattern Unification"	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6901: [compat] Remove "Injection L2R Pattern Order"	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[toplevel] Modify printing goal strategy.	Emilio Jesus Gallego Arias	2018-03-05
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fix failing packaging job.	Théo Zimmermann	2018-03-05
\| \|_\|_\|_\|_\|_\|_\|/ / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Remove NOPLUGINDOCS option	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Add empty description for @raise statements to satisfy ocamldoc	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Escape curly braces in ocamldoc comment	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Separate vim/emacs fold markers from ocamldoc comments	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Build docs for plugins by default, add NOPLUGINDOCS flag to disable	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Change non-documentation comment from ocamldoc style	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Fix formatting of some ocamldoc comments to reduce warnings	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Replace invalid tag @raises in ocamldoc comments with @raise	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Remove non-existent dependency	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Tweak comments to fix ocamldoc errors	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Tidy up ml-doc outut, give it a separate output directory	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Use computed deps to generate ml-doc and use implicit mli-doc deps	mrmr1993	2018-03-05
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	CHANGES and tests for with Definition @{univs}	Gaëtan Gilbert	2018-03-05
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Allow universe declarations for [with Definition].	Gaëtan Gilbert	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Deprecate Focus and Unfocus.	Théo Zimmermann	2018-03-05
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[ssreflect] Export parsing witnesses in mli file.	Emilio Jesus Gallego Arias	2018-03-05
\| \|_\|_\|_\|_\|/ / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Sanitize universe declaration in Context (stop using a ref...)	Gaëtan Gilbert	2018-03-05
\| \| \| \| \| \| \| \|/ / / / / / / / / / / / / /