coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
\| \| \| \|	The removed code isn't used locally and isn't exported in the signature
*	Adding a generic Int.Map using persistent arrays.	Pierre-Marie Pédrot	2013-11-26
\|
*	Manual coding of Int.Map.find. We use unsafe features, but this function	ppedrot	2013-11-04
\| \| \| \| \| \| \|	is quite critical indeed, as it is one of the most used throughout Coq executions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17050 85f007b7-540e-0410-9357-904b9bb8a0f7
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
\| \| \| \| \| \| \| \| \| \| \|	To reduce the amount of syntactic noise, we now provide a few inner modules Int.List, Id.List, String.List, Sorts.List which contain some monomorphic (or semi-monomorphic) functions such as mem, assoc, ... NB: for Int.List.mem and co we reuse List.memq and so on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16936 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Specializing hash functions for widely used types.	ppedrot	2013-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16933 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a more efficient way to recover the domain of a map.	ppedrot	2013-08-25
\| \| \| \| \| \| \| \| \| \|	The extended signature is defined in CMap, and should be compatible with the old one, except that module arguments have to be explicitely named. The implementation itself is quite unsafe, as it relies on the current implementation of OCaml maps, even though that should not be a problem (it has not changed in ages). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16735 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Moved Intset and Intmap to Int namespace.	ppedrot	2012-12-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16067 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added an Int module with dummy utility functions.	ppedrot	2012-11-08
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15956 85f007b7-540e-0410-9357-904b9bb8a0f7