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-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-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-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
	With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
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-06-22	New script dev/tools/change-header to automatically update Coq files headers.	herbelin
	Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 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
2010-04-29	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill
	dev/ocamlweb-doc has been erased. I hope no one still use the "new-parse" it generate. In dev/, make html will generate in dev/html/ "clickable version of mlis". (as the caml standard library) make coq.pdf will generate nearly the same awfull stuff that coq.ps was. make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of the given directory. ocamldoc comment syntax is here : http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html The possibility to put graphs in pdf/html seems to be lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 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
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