coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-02-27	Update headers following #6543.	Théo Zimmermann

2017-12-09	Remove most uses of function extensionality in Program.Combinators	Jasper Hugunin

2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2016-01-20	Update copyright headers.	Maxime Dénès

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

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-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-28	Fix the stdlib doc compilation + switch all .v file to utf8	letouzey
	1) compilation of Library.tex was failing on a "Ext_" in Diaconescu.v In fact coqdoc was trying to recognize the end of a _emphasis_ and hence inserted a bogus }. For the moment I've enclosed the phrase with [ ], but this emphasis "feature" of coqdoc seems _really_ easy to broke. Matthieu ? 2) By the way, this Library document was made from latin1 and utf8 source file, hence bogus characters. All .v containing special characters are converted to utf8, and their first line is now mentionning this. (+ killed some old french comments and some other avoidable special characters). PLEASE: let's stick to this convention and avoid latin1, at least in .v files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12363 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-12-16	Move FunctionalExtensionality to Logic/ (someone please check that the	msozeau
	doc is ok). Rework the .v files in Program accordingly, adding some documentation and proper headers. Integrate the development of an elimination principle for measured functions in Program/Wf by Eelis van der Weegen. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11686 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-16	Reorganize Program and Classes theories. Requiring Setoid no longer sets	msozeau
	implicits for left, inl or eq, hence some theories had to be changed again. It should make some user contribs compile again too. Also do not import functional extensionality when importing Program.Basics, add a Combinators file for proofs requiring it and a Syntax file for the implicit settings. Move Classes.Relations to Classes.RelationClasses to avoid name clash warnings as advised by Hugo and Pierre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10681 85f007b7-540e-0410-9357-904b9bb8a0f7