diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-14 12:41:32 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-14 12:41:32 +0000 |
| commit | 94eed81b4fbea5bf05e722280a9338ca607e2f21 (patch) | |
| tree | 6d932d03cf6d3ea0910d51418455b2138488738b /plugins/extraction/big.ml | |
| parent | 1d0e61fe25ffaec80bcc175df94797d8a9fdc868 (diff) | |
Update of Extraction documentation
- 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
Diffstat (limited to 'plugins/extraction/big.ml')
0 files changed, 0 insertions, 0 deletions