coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	use Int.equal instead of polymorphic =	Paul Steckler	2017-07-05
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-30
\|\
\| *	A patch renaming equal into eq in the module dealing with	Hugo Herbelin	2016-03-22
\| \| \| \| \| \| \| \| \| \|	hash-consing, so as to avoid having too many kinds of equalities with same name.
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
\| \|
* \|	Avoid warnings about loop indices.	Guillaume Melquiond	2016-01-02
\| \|
\| *	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin	2015-08-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Sorry so much. Reverted: 707bfd5719b76d131152a258d49740165fbafe03. 164637cc3a4e8895ed4ec420e300bd692d3e7812. b9c96c601a8366b75ee8b76d3184ee57379e2620. 21e41af41b52914469885f40155702f325d5c786. 7532f3243ba585f21a8f594d3dc788e38dfa2cb8. 27fb880ab6924ec20ce44aeaeb8d89592c1b91cd. fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c. d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962. 6737055d165c91904fc04534bee6b9c05c0235b1. 342fed039e53f00ff8758513149f8d41fa3a2e99. 21525bae8801d98ff2f1b52217d7603505ada2d2. b78d86d50727af61e0c4417cf2ef12cbfc73239d. 979de570714d340aaab7a6e99e08d46aa616e7da. f556da10a117396c2c796f6915321b67849f65cd. d8226295e6237a43de33475f798c3c8ac6ac4866. fdab811e58094accc02875c1f83e6476f4598d26.
\| *	A patch renaming equal into eq in the module dealing with	Hugo Herbelin	2015-08-02
\|/ \| \| \| \|	hash-consing, so as to avoid having too many kinds of equalities with same name.
*	Adding a statistic function on hashconsing tables.	Pierre-Marie Pédrot	2015-02-11
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Removing the call to Weak.get_copy in hashsets.	Pierre-Marie Pédrot	2014-07-31
\| \| \| \| \| \| \| \| \| \| \| \|	The rationale for its use comes from OCaml weak maps, and is justified by the fact that Weak.get may prevent its return value to be collected by the GC during the next slice even though nobody points to it. In our case, this is vastly irrelevant because hashconsed values are not expected to be collected whatsoever (save for exceptional cases). But Weak.get_copy is rather costly actually, at least strictly more than the plain Weak.get. Experimentally, I observe diminution of compilation time and even diminution of memory consumption (!) after this patch, so I assume it is a net gain.
*	Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to	Hugo Herbelin	2014-04-28
\| \| \| \| \| \| \| \| \| \|	one_inductive_body so that when eta-expanding at "match" printing time we know if a let is part of the expected signature or part of the body. This is an easy fix for bugs like #3293. Another fix could be to enforce, as an invariant, or better syntactically, that "match"/"Case"'s have the body of their branches expanded.
*	Tweaking arity & allocation of some basic functions.	Pierre-Marie Pédrot	2013-11-24
\|
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵	xclerc	2013-09-19
\| \| \| \| \| \|	with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removed many calls to OCaml generic equality. This was done by	ppedrot	2012-10-29
\| \| \| \| \| \| \| \|	writing our own comparison functions, and enforcing monomorphization in many places. This should be more efficient, btw. Still a work in progress. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15932 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Using weak tables instead of plain hash tables while hashconsing.	ppedrot	2012-10-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15899 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reusing the Hashset data structure in Hashcons. Hopefully, this should	ppedrot	2012-09-26
\| \| \| \| \| \|	not disrupt anything... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15836 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cleaning, renaming obscure functions and documenting in Hashcons.	ppedrot	2012-09-26
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15834 85f007b7-540e-0410-9357-904b9bb8a0f7