diff options
| author | Clément Pit-Claudel | 2020-03-19 18:42:10 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-03-19 18:42:10 -0400 |
| commit | 47d92a69773755e2ad5d5f987f87337fdf7e98d8 (patch) | |
| tree | 3a074b1269952ef2cbbb4d5fce64531580c61443 /doc/sphinx/addendum | |
| parent | 9f680f776140c8b3b8f79013262d5bd73761d571 (diff) | |
| parent | 1be31dea4cfd31522898edc07fee0829fea7c68d (diff) | |
Merge PR #11601: [refman] Move chapters into new structure.
Reviewed-by: jfehrle
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/addendum/miscellaneous-extensions.rst | 7 |
2 files changed, 3 insertions, 8 deletions
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index d909f98956..41b726b069 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -1,7 +1,7 @@ .. _extraction: -Extraction of programs in |OCaml| and Haskell -============================================= +Program extraction +================== :Authors: Jean-Christophe Filliâtre and Pierre Letouzey diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index db8c09d88f..0e8660cb0e 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -1,10 +1,5 @@ -.. _miscellaneousextensions: - -Miscellaneous extensions -======================== - Program derivation ------------------- +================== |Coq| comes with an extension called ``Derive``, which supports program derivation. Typically in the style of Bird and Meertens or derivations |