coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-27
\|\
\| *	Reference Manual / Extraction: the original example command no longer works ↵	Matej Kosik	2016-06-20
\| \| \| \| \| \| \| \|	with recent Coq
* \|	typography	Matej Kosik	2016-06-15
\|/
*	Extraction: documentation of the new option Unset Extraction SafeImplicits	Pierre Letouzey	2015-12-12
\|
*	Fix typos in the Extraction part of the reference manual.	Guillaume Melquiond	2015-07-31
\| \| \| \|	In particular, fix the name of all the user contributions.
*	Separate index for vernacular options.	Maxime Dénès	2015-02-17
\|
*	Fix some documentation typos.	Guillaume Melquiond	2015-01-08
\|
*	refman: switch all source files to utf8	Pierre Letouzey	2014-12-09
\| \| \| \| \| \|	Putting utf8 everywhere helps the maintainance of the online refman. And anyway, this is the way to go. We should also chase and migrate the few remaining iso-latin-1 files elsewhere in the sources.
*	"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).
*	Add option Set/Unset Extraction Conservative Types.	aspiwack	2012-08-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Extracted code need not preserve typing relations (e:t) from the source code. This may be a problem as the extracted code may not implement the intented interface. This option disables the optimisations which would prevent an extracted term's type to be its extracted source term's type. At this point the only such optimization is (I think) removing some dummy λ-abstractions in constant definitions. Extraction Implicit is still honored in this mode, and it's mostly necessary to produce reasonable types. So in the conservative type mode, which abstractions can be removed and which can'tt is entirely under the user's control. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15762 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extraction: document Separate Extraction and KeepSingleton	letouzey	2012-08-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15746 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extraction.tex: typo in an Extract Inductive example (fix #2625)	letouzey	2011-10-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14574 85f007b7-540e-0410-9357-904b9bb8a0f7
*	doc/refman/Extraction.tex: no need to actually build euclid.ml	letouzey	2011-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14478 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Update of Extraction documentation	letouzey	2010-06-14
\| \| \| \| \| \| \| \| \| \| \| \|	- Removal of the notice about the "experimental" status of extraction. Of course extraction is still experimental, but no less than the rest of Coq ;-) - Removal of the example about heapsort now that Heap is obsolete. - Euclid isn't the best of the examples, but for the moment we leave it - We mention ExtrOcamlIntConv and the others extraction/*.v - Various small improvements git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13136 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extraction Implicit: documentation	letouzey	2010-06-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13133 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extract Inductive is now possible toward non-inductive types (e.g. nat => int)	letouzey	2010-05-21
\| \| \| \| \| \| \| \| \| \| \|	For instance: Extract Inductive nat => int [ "0" "succ" ] "(fun fO fS n => if n=0 then fO () else fS (n-1))". See Extraction.v for more details and caveat. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13025 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
\| \| \| \| \| \| \| \| \| \| \|	- 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
*	Removed 'Toplevel' language from extraction documentation, since it is not ↵	gmelquio	2009-11-04
\| \| \| \| \| \|	currently supported. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12467 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed some typos in the reference manual.	gmelquio	2009-10-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12443 85f007b7-540e-0410-9357-904b9bb8a0f7
*	typo in doc of Extraction Blacklist	letouzey	2009-10-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12394 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵	letouzey	2009-03-20
\| \| \| \| \| \|	user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extraction Blacklist : a new command for avoiding conflicts with existing files	letouzey	2008-12-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11690 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Standardisation du format des références croisées vers Figure, Section, ↵	herbelin	2008-01-05
\| \| \| \| \| \| \| \| \| \| \|	Chapter Remplacement pageref par ref parce que pageref n'a pas de sens pour la version HTML git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10421 85f007b7-540e-0410-9357-904b9bb8a0f7
*	documentation of commit 10188	letouzey	2007-10-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10198 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification des propriétés des fichiers .tex (svn:executable)	notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty	2006-02-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8609 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage de l'archive doc et restructuration avant intégration à l'archive	herbelin	2006-02-23
	principale de Coq et publication des sources (HH) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8606 85f007b7-540e-0410-9357-904b9bb8a0f7