coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-01-20	Update copyright headers.	Maxime Dénès

2015-01-12	Update headers.	Maxime Dénès

2014-10-10	Fix segfault in native compiler on int31 division.	Maxime Dénès
	Thanks to Yves for reporting it!
2014-09-24	Make the retroknowledge marshalable.	Arnaud Spiwack
	Essential for parallel processing of Coq documents. It is a fairly straightforward change but a tad tedious, I may have introduced some bugs in the process.
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-04-09	Machine arithmetic operations for native compiler.	Maxime Dénès
	This completes the port of the native compiler to retroknowledge. However, some testing and optimizations are still to be done.
2014-04-09	Full support for int31 values in native compiler.	Maxime Dénès

2014-04-09	Partial support for open terms in int31.	Maxime Dénès

2014-04-09	Had to split Nativelambda in two files because of Retroknowledge	Maxime Dénès
	dependencies.
2014-04-09	Int31 literals in native compiler.	Maxime Dénès

2014-03-14	Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it had	Pierre-Marie Pédrot
	no particular purpose.
2014-03-03	Fixing pervasive equalities. In particular, I removed the code that deleted	Pierre-Marie Pédrot
	duplicates in kernel side effects. They were chosen according to an equality that was quite irrelevant, and as expected this patch did not break the test-suite.
2012-09-14	This patch removes unused "open" (automatically generated from	regisgia
	compiler warnings). I was afraid that such a brutal refactoring breaks some obscure invariant about linking order and side-effects but the standard library still compiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-11	fast bitwise operations (lor,land,lxor) on int31 and BigN	letouzey
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15727 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08	Updating headers.	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-09	Added a few informations about file lineages (for the most part in kernel)	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13005 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
	- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-08	Some dead code removal + cleanups	letouzey
	This commit concerns about the first half of the useless code mentionned by Oug for coqtop (without plugins). For the moment, Oug is used in a mode where any elements mentionned in a .mli is considered to be precious. This already allows to detect and remove about 600 lines, and more is still to come. Among the interesting points, the type Entries.specification_entry and its constructors SPExxx were never used. Large parts of cases.ml (and hence subtac_cases.ml) were also useless. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12069 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-01	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin
	pas correctes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10739 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-20	ajout de head0 et tail0 en natif	bgregoir
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9900 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-11	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack
	details). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7