diff options
| author | Vincent Laporte | 2019-06-25 09:10:44 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-07-22 12:17:53 +0000 |
| commit | c878a5e2c0c2a01512e263d3ed2dfdd8e611086f (patch) | |
| tree | 90191993778dcf27e3ecaf5c43040cd57a69646d /doc/changelog/08-tools | |
| parent | 033021860b2ea6fee901f6c760dcd8292ed07fe5 (diff) | |
[Extraction] Add support for primitive integers
The ExtrOCamlInt63 module can be required to map primitives from the Int63
module to their OCaml implementation (module Uint63 from the kernel).
Diffstat (limited to 'doc/changelog/08-tools')
| -rw-r--r-- | doc/changelog/08-tools/10430-extraction-int63.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/changelog/08-tools/10430-extraction-int63.rst b/doc/changelog/08-tools/10430-extraction-int63.rst new file mode 100644 index 0000000000..68ae4591a4 --- /dev/null +++ b/doc/changelog/08-tools/10430-extraction-int63.rst @@ -0,0 +1,5 @@ +- Fix extraction to OCaml of primitive machine integers; + see :ref:`primitive-integers` + (`#10430 <https://github.com/coq/coq/pull/10430>`_, + fixes `#10361 <https://github.com/coq/coq/issues/10361>`_, + by Vincent Laporte). |