coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	use OCaml 4.03-compatible Filename functions	Paul Steckler	2017-08-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Prevent overallocation in Array.map_to_list and remove custom implementation ↵	Guillaume Melquiond	2017-08-22
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	from Detyping.
\| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Fix obsolete description of real numerals.	Guillaume Melquiond	2017-08-22
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \|	Fix coqdoc URLs under Windows.	Théo Zimmermann	2017-08-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	URLs on Windows are the same as on Unix, they use / not \.
\| * \| \| \| \| \| \| \| \| \| \| \| \|	Extend .gitignore for coqdoc test-suite.	Théo Zimmermann	2017-08-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \|	Fix coqdoc test-suite target on Windows.	Théo Zimmermann	2017-08-21
\|/ / / / / / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Commit 8f12597 introduced new output tests but these were broken on Windows. We fix them by using --strip-trailing-cr option of diff, like in other output tests in the test-suite.
\| \| \| \| \| \| \| \| \| * \| \| \|	use OCaml temp_file, instead of our own version	Paul Steckler	2017-08-18
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \|	add CHANGES entry	Paul Steckler	2017-08-18
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \|	move filename search to start_profiler	Paul Steckler	2017-08-18
\| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #965: Moving file primitive.ml to cPrimitive.ml to avoid conflict ↵	Maxime Dénès	2017-08-18
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	with OCaml.
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #983: Correct the option for cumulativity in CHANGES	Maxime Dénès	2017-08-18
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #973: Adding documentation for Printing Focused option.	Maxime Dénès	2017-08-18
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Correct the option for cumulativity in CHANGES	Amin Timany	2017-08-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #801: Make Travis generate OSX packages.	Maxime Dénès	2017-08-18
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|/ / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Don't belittle the size of the SE community	Tej Chajed	2017-08-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Separate jobs for test-suite and package building under OSX.	Maxime Dénès	2017-08-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Don't mention coq-club at all	Tej Chajed	2017-08-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Advise contributors to use SE over coq-club	Tej Chajed	2017-08-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Add native compute profiling, BZ#5170	Paul Steckler	2017-08-17
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #972: 8.7 change entries	Maxime Dénès	2017-08-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #490: A possible fix for #5391 (command line tools do not accept ↵	Maxime Dénès	2017-08-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	trailing / and \ on windows)
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #974: Change section caption, improve some wording	Maxime Dénès	2017-08-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #976: Document anonymous universes (PR #544).	Maxime Dénès	2017-08-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Use the wording suggested by Gaetan.	Théo Zimmermann	2017-08-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Addition suggested by Pierre-Marie.	Théo Zimmermann	2017-08-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Change 8.7~alpha to 8.7+alpha.	Maxime Dénès	2017-08-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Only the latter is a valid git tag, and we will soon be using those to generate our version numbers.
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Make Travis generate OSX packages.	Maxime Dénès	2017-08-17
\| \|_\|_\|_\|/ / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The packages will be built only for main branches (not pull requests), and are accessible via bintray: https://bintray.com/coq/coq
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Document anonymous universes (PR #544).	Gaëtan Gilbert	2017-08-17
\|/ / / / / / / / / / / / / / / / /
\| \| \| \| * / / / / / / / / / / / /	Adding documentation for Printing Focused option.	Pierre Courtieu	2017-08-17
\| \|_\|_\|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Additions following Hugo's suggestions.	Théo Zimmermann	2017-08-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	mention that tactic is the identity or gives error	Paul Steckler	2017-08-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Improve wording.	Théo Zimmermann	2017-08-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Mention tclINDEPENDENTL (#349) in dev/doc/changes.	Théo Zimmermann	2017-08-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	8.7 CHANGES	Théo Zimmermann	2017-08-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	change section caption, improve some wording	Paul Steckler	2017-08-16
\|/ / / / / / / / / / / / / / /
\| \| * / / / / / / / / / / / /	Porting #856 (8.6.1 CHANGES entries) to master	Théo Zimmermann	2017-08-16
\| \|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #957: Set detachable windows type hint to dialog.	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #831: Port ssreflect user manual to Coq's latex/hevea style	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #912: Detyping functions are now operating on EConstr.t.	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #942: solving b1859	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #954: Print names of all open blocks	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #964: More portable location for the time command.	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #951: Makefile: install-byte works even if -coqide no	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #841: Timorous fix of bug #5598 on global existing class in sections	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #948: [doc] Write (@nil nat) instead of (nil nat)	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #944: Fix typos. Improve wording.	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #943: Reference Manual: minor wording improvements	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #940: Replace jarring use of "Remark" with "Note"	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #934: Fix some coq-tex errors in the reference manual.	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords ↵	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	wrongly tagged as keywords