coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	test-suite/output-modulo-time made more robust	Enrico Tassi	2016-09-30
\| \| \| \|	Order of items made stable
*	Merge remote-tracking branch 'github/pr/303' into v8.6	Maxime Dénès	2016-09-30
\|\ \| \| \| \| \| \|	Was PR#303: LtacProf cutoff is for total percent, not time
\| *	LtacProf cutoff is for total percent, not time	Jason Gross	2016-09-29
\| \|
* \|	Set the default LtacProf cutoff to 2%	Jason Gross	2016-09-29
\|/ \| \| \| \| \| \| \| \| \| \|	This was the original value from Tobias' code. When a user passes -profile-ltac on the command line, or inserts [Show Ltac Profile] in the document, the most useful default behavior is to not overload them with useless information. When GUI clients want to display fancier profiling information, there is no cost to the user to requiring them to specify what cutoff they want. If the GUI client does not have any special LtacProf handling, the most useful presentation is again the one that cuts off the display at 2% total time.
*	Add support for testing output mod timing changes	Jason Gross	2016-09-11
	Uses sed 's/\s[0-9]\.[0-9]\+\s//g' and 's/\s0\.\s*//g' to strip numbers of seconds and to strip percentages. (This can potentially be extended later.) Add a test-suite file to make sure that LtacProf outputs some table.