aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/Extraction.tex
Commit message (Expand)AuthorAge
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 03:41:00 +0000