coq - The formal proof system

Age	Commit message (Collapse)	Author
2015-02-24	New function [Constr.equal_with] to compare terms up to variants of ↵	Arnaud Spiwack
	[kind_of_term]. To be able to write equality up to evar instantiation instantiation. Generalises the main function of [eq] constr over the variant of [kind_of_term] it uses. It prevents some optimisation of [Array.equal] where two physically equal arrays are considered (less or) equal. But it does not seem to have appreciable effects on efficiency.
2014-10-05	A few improvements on pattern-matching compilation.	Hugo Herbelin
	- Optimize the removal of generalization when there is no dependency in the generalized variable (see postprocess_dependencies, and the removal of dependencies in the default type of impossible cases). - Compute the onlydflt flag correctly (what allows automatic treatment of impossible cases even when there is no clause at all).
2014-08-25	"allows to", like "allowing to", is improper	Jason Gross
	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).
2014-03-02	Set officially the minimal OCaml requirement to 3.12.1	Pierre Letouzey
	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 ;-)
2014-02-09	Small optimizations in Closure:	Pierre-Marie Pédrot
	1. Only apply last Zupdates 2. Better smartmap with state.
2013-11-04	Adding closure-preventing functions in CArray. These functions are all	ppedrot
	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
2013-10-23	Small optimizations in unification.	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16918 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22	More efficient operations in CArray.	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16910 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-05	Missing primitive in CArray	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16259 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-19	Array.create is deprecated	pboutill
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16104 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-25	Fixing ocamldoc errors	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15833 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-18	More cleaning in CArray...	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15819 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7