coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	add CHANGES entry	Paul Steckler	2017-08-18
*	move filename search to start_profiler	Paul Steckler	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 tra...	Maxime Dénès	2017-08-17
\|\ \
* \ \	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
\| * \| \| \|	Document anonymous universes (PR #544).	Gaëtan Gilbert	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 wr...	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #864: Some cleanups after cumulativity for inductive types	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Removing trailing "/" and "\" in directory names only on win32.	Hugo Herbelin	2017-08-15
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Adding a test for BZ#1859 as suggested by @tchajed.	Théo Zimmermann	2017-08-15
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #963: fix coq_makefile	Maxime Dénès	2017-08-12
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	fix coq_makefile	Matej Košík	2017-08-12
\|/ / / / / / / / / / / / / / / / /
\| \| \| \| \| \| \| \| \| \| * / / / / / /	More portable location for the time command.	Théo Zimmermann	2017-08-12
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Set detachable windows type hint to dialog.	Olivier Marty	2017-08-08
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Print names of all open blocks	Tej Chajed	2017-08-06
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \|	Makefile: install-byte works even if -coqide no	Enrico Tassi	2017-08-04
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \|	Amend wording to capture intended meaning	Sam Pablo Kuper	2017-08-03
\| \| \| \| \| \| \| \| \| \| \| * \|	Rewording the introduction	Enrico Tassi	2017-08-02
\| \| \| \| \| \| \| \| \| \| \| * \|	Rephrasing a couple of sentences in a more factual way.	Hugo Herbelin	2017-08-02
\| \| \| \| \| \| \| \| \| \| \| * \|	Rephrasing the introduction in a more factual and up-to-date way.	Hugo Herbelin	2017-08-02
\| \| \| \| \| \| \| \| \| \| \| * \|	Port ssr manual to Coq's latex/hevea style	Enrico Tassi	2017-08-02
\| \| \| \| \| \| \| \| \| \| \| * \|	Makefile.doc: implement serve-refman-8080 target	Enrico Tassi	2017-08-02
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \|	Update Setoid.tex	larsr	2017-08-02
\| \|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Makefile: 'make clean' now immune to the check for binary files without sources	Pierre Letouzey	2017-08-02
\| * \| \| \| \| \| \| \| \| \|	Typo in the documentation of cumulativity	Amin Timany	2017-08-02
\| \| \| \| \| \| \| \| \| * \|	Printing goals does not evar-normalizes beforehand anymore.	Pierre-Marie Pédrot	2017-08-01