coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
\| \| \| \| \| \| \| \| \| \| \|	It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar).
*	Set officially the minimal OCaml requirement to 3.12.1	Pierre Letouzey	2014-03-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Anyway, a few syntactic features of 3.12 were already used here and there (e.g. local opening via Foo.(...), or the record shortcut { field; ... }). Hence compiling with 3.11 wasn't working anymore. Already take advantage of the following 3.12.1 features : - "module type of ..." in CArray, CList, CString ... - "ocamldep -ml-synonym" : no need anymore to hack the ocamldep output via our coqdep to localize the .ml4 modules :-) The -ml-synonym option (+ various bugfixes) is the reason for asking 3.12.1 directly and not just 3.12.0. After all, if debian stable is providing 3.12.1, then everybody has it ;-)
*	Small optimizations in Closure:	Pierre-Marie Pédrot	2014-02-09
\| \| \| \| \|	1. Only apply last Zupdates 2. Better smartmap with state.
*	Adding closure-preventing functions in CArray. These functions are all	ppedrot	2013-11-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	higher-order functions like map and iter, and they are modified so that they take one additional argument, thus saving a cloure allocation. Compare the following. Array.iter: ('a -> unit) -> 'a array -> unit Array.Fun1.iter: ('r -> 'a -> unit) -> 'r -> 'a array -> unit Basically, Array.Fun1.iter f x v = Array.iter (f x) v, though it does not allocate a closure. For now only the most critical functions are recoded. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17053 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Small optimizations in unification.	ppedrot	2013-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16918 85f007b7-540e-0410-9357-904b9bb8a0f7
*	More efficient operations in CArray.	ppedrot	2013-10-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16910 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Missing primitive in CArray	ppedrot	2013-03-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16259 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Array.create is deprecated	pboutill	2012-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16104 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing ocamldoc errors	ppedrot	2012-09-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15833 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
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7