aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/Extraction.tex
Commit message (Expand)AuthorAge
* Avoid generated names for html pages of the reference manual (bug #4742).Gravatar Guillaume Melquiond2017-09-22
* Merge PR #934: Fix some coq-tex errors in the reference manual.Gravatar Maxime Dénès2017-08-16
|\
| * Fix some coq-tex errors in the reference manual.Gravatar Guillaume Melquiond2017-07-28
* | Extraction.tex: mention the possible "From Coq Require Extraction"Gravatar letouzey2017-07-27
* | Extraction TestCompile documented + mentionned in CHANGESGravatar Pierre Letouzey2017-07-27
|/
* Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\
| * Reference Manual / Extraction: the original example command no longer works w...Gravatar Matej Kosik2016-06-20
* | typographyGravatar Matej Kosik2016-06-15
|/
* Extraction: documentation of the new option Unset Extraction SafeImplicitsGravatar Pierre Letouzey2015-12-12
* Fix typos in the Extraction part of the reference manual.Gravatar Guillaume Melquiond2015-07-31
* Separate index for vernacular options.Gravatar Maxime Dénès2015-02-17
* Fix some documentation typos.Gravatar Guillaume Melquiond2015-01-08
* refman: switch all source files to utf8Gravatar Pierre Letouzey2014-12-09
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Add option Set/Unset Extraction Conservative Types.Gravatar aspiwack2012-08-24
* Extraction: document Separate Extraction and KeepSingletonGravatar letouzey2012-08-23
* Extraction.tex: typo in an Extract Inductive example (fix #2625)Gravatar letouzey2011-10-18
* doc/refman/Extraction.tex: no need to actually build euclid.mlGravatar letouzey2011-09-17
* Update of Extraction documentationGravatar letouzey2010-06-14
* Extraction Implicit: documentationGravatar letouzey2010-06-14
* Extract Inductive is now possible toward non-inductive types (e.g. nat => int)Gravatar letouzey2010-05-21
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Removed 'Toplevel' language from extraction documentation, since it is not cu...Gravatar gmelquio2009-11-04
* Fixed some typos in the reference manual.Gravatar gmelquio2009-10-29
* typo in doc of Extraction BlacklistGravatar letouzey2009-10-15
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20
* Extraction Blacklist : a new command for avoiding conflicts with existing filesGravatar letouzey2008-12-16
* Standardisation du format des références croisées vers Figure, Section, Ch...Gravatar herbelin2008-01-05
* documentation of commit 10188Gravatar letouzey2007-10-08
* Modification des propriétés des fichiers .tex (svn:executable)Gravatar notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty2006-02-24
* Nettoyage de l'archive doc et restructuration avant intégration à l'archiveGravatar herbelin2006-02-23