aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/Extraction.tex
AgeCommit message (Expand)Author
2018-03-29[Sphinx] Move chapter 23 to new infrastructureMaxime Dénès
2017-12-05use \ocaml macro in Extraction chapter; accept OCaml in Extraction LanguagePaul Steckler
2017-11-28use \ocaml macro in new textPaul Steckler
2017-11-22use OCaml criteria for infix ops, #6212Paul Steckler
2017-09-22Avoid generated names for html pages of the reference manual (bug #4742).Guillaume Melquiond
2017-08-16Merge PR #934: Fix some coq-tex errors in the reference manual.Maxime Dénès
2017-07-28Fix some coq-tex errors in the reference manual.Guillaume Melquiond
2017-07-27Extraction.tex: mention the possible "From Coq Require Extraction"letouzey
2017-07-27Extraction TestCompile documented + mentionned in CHANGESPierre Letouzey
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
2016-06-27Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-20Reference Manual / Extraction: the original example command no longer works w...Matej Kosik
2016-06-15typographyMatej Kosik
2015-12-12Extraction: documentation of the new option Unset Extraction SafeImplicitsPierre Letouzey
2015-07-31Fix typos in the Extraction part of the reference manual.Guillaume Melquiond
2015-02-17Separate index for vernacular options.Maxime Dénès
2015-01-08Fix some documentation typos.Guillaume Melquiond
2014-12-09refman: switch all source files to utf8Pierre Letouzey
2014-08-25"allows to", like "allowing to", is improperJason Gross
2012-08-24Add option Set/Unset Extraction Conservative Types.aspiwack
2012-08-23Extraction: document Separate Extraction and KeepSingletonletouzey
2011-10-18Extraction.tex: typo in an Extract Inductive example (fix #2625)letouzey
2011-09-17doc/refman/Extraction.tex: no need to actually build euclid.mlletouzey
2010-06-14Update of Extraction documentationletouzey
2010-06-14Extraction Implicit: documentationletouzey
2010-05-21Extract Inductive is now possible toward non-inductive types (e.g. nat => int)letouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-11-04Removed 'Toplevel' language from extraction documentation, since it is not cu...gmelquio
2009-10-29Fixed some typos in the reference manual.gmelquio
2009-10-15typo in doc of Extraction Blacklistletouzey
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2008-12-16Extraction Blacklist : a new command for avoiding conflicts with existing filesletouzey
2008-01-05Standardisation du format des références croisées vers Figure, Section, Ch...herbelin
2007-10-08documentation of commit 10188letouzey
2006-02-24Modification des propriétés des fichiers .tex (svn:executable)notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty
2006-02-23Nettoyage de l'archive doc et restructuration avant intégration à l'archiveherbelin