coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Tweaking arity & allocation of some basic functions.	Pierre-Marie Pédrot	2013-11-24
\|
*	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
*	Fix the semantic of the new List.remove_assoc_f	letouzey	2013-10-24
\| \| \| \| \| \| \|	Unlike Ocaml's stdlib List.remove_assoc, I was raising Not_found when the key to remove wasn't there... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16931 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Turn many List.assoc into List.assoc_f	letouzey	2013-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16925 85f007b7-540e-0410-9357-904b9bb8a0f7
*	cList: a few alternative to hashtbl-based uniquize, distinct, subset	letouzey	2013-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16924 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CList.factorize_left with a parametric equality	letouzey	2013-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16923 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CList.prefix_of and CList.drop_prefix with a parametric equality	letouzey	2013-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16922 85f007b7-540e-0410-9357-904b9bb8a0f7
*	cList.index is now cList.index_f, same for index0	letouzey	2013-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16921 85f007b7-540e-0410-9357-904b9bb8a0f7
*	cList: set-as-list functions are now with an explicit comparison	letouzey	2013-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Optimizing evar filters. It seems to cost quite a lot in unification,	ppedrot	2013-10-22
\| \| \| \| \| \| \|	as witnessed by profiling on time-consuming files. I suspect we can do better by using a smarter representation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16912 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Clib: fold_left_until added to CList	gareuselesinge	2013-10-10
\| \| \| \| \| \| \|	CStack just calls it to implement fold_until. CSig.seek renamed CSig.until, since there is no seek function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16867 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removing some lone List.assoc & List.mem in lib.	ppedrot	2013-08-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16738 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Minor code cleaning in CArray / CList.	ppedrot	2013-03-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16351 85f007b7-540e-0410-9357-904b9bb8a0f7
*	invalid_arg instead of raise (Invalid_argement ...)	letouzey	2013-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16270 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Monomorphization (lib)	ppedrot	2012-11-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15991 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cleaning and small optimization in CList.	ppedrot	2012-11-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15988 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	the new Int module. Only the most obvious were removed, so there are a lot more in the wild. This may sound heavyweight, but it has two advantages: 1. Monomorphization is explicit, hence we do not miss particular optimizations of equality when doing it carelessly with the generic equality. 2. When we have removed all the generic equalities on integers, we will be able to write something like "let (=) = ()" to retrieve all its other uses (mostly faulty) spread throughout the code, statically. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
*	More cleaning in CArray...	ppedrot	2012-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15819 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cleaning interface of Util.	ppedrot	2012-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15817 85f007b7-540e-0410-9357-904b9bb8a0f7
*	More cleaning on Utils and CList. Some parts of the code being	ppedrot	2012-09-17
\| \| \| \| \| \|	peculiarly messy, I hope I did not introduce too many bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15815 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Some documentation and cleaning of CList and Util interfaces.	ppedrot	2012-09-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15805 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added some tricky tail-rec versions of List functions to CList	ppedrot	2012-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15803 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
	List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7