index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
doc
/
refman
/
Extraction.tex
Commit message (
Expand
)
Author
Age
*
Add option Set/Unset Extraction Conservative Types.
aspiwack
2012-08-24
*
Extraction: document Separate Extraction and KeepSingleton
letouzey
2012-08-23
*
Extraction.tex: typo in an Extract Inductive example (fix #2625)
letouzey
2011-10-18
*
doc/refman/Extraction.tex: no need to actually build euclid.ml
letouzey
2011-09-17
*
Update of Extraction documentation
letouzey
2010-06-14
*
Extraction Implicit: documentation
letouzey
2010-06-14
*
Extract Inductive is now possible toward non-inductive types (e.g. nat => int)
letouzey
2010-05-21
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Removed 'Toplevel' language from extraction documentation, since it is not cu...
gmelquio
2009-11-04
*
Fixed some typos in the reference manual.
gmelquio
2009-10-29
*
typo in doc of Extraction Blacklist
letouzey
2009-10-15
*
Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...
letouzey
2009-03-20
*
Extraction Blacklist : a new command for avoiding conflicts with existing files
letouzey
2008-12-16
*
Standardisation du format des références croisées vers Figure, Section, Ch...
herbelin
2008-01-05
*
documentation of commit 10188
letouzey
2007-10-08
*
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
*
Nettoyage de l'archive doc et restructuration avant intégration à l'archive
herbelin
2006-02-23