<feed xmlns='http://www.w3.org/2005/Atom'>
<title>coq/theories/extraction, branch master</title>
<subtitle>The formal proof system</subtitle>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/'/>
<entry>
<title>Replace mentions of Num by Zarith.</title>
<updated>2021-03-28T15:12:49+00:00</updated>
<author>
<name>Guillaume Melquiond</name>
</author>
<published>2021-03-28T15:12:49+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=58f35aad952c94744f232b622ab07ffb5d932a15'/>
<id>58f35aad952c94744f232b622ab07ffb5d932a15</id>
<content type='text'>
The documentation of extraction became outdated when the big.ml wrapper
got modified by 094e4649c29e2426daca0476c140439de901dafe.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
The documentation of extraction became outdated when the big.ml wrapper
got modified by 094e4649c29e2426daca0476c140439de901dafe.
</pre>
</div>
</content>
</entry>
<entry>
<title>Signed primitive integers</title>
<updated>2021-02-26T13:32:41+00:00</updated>
<author>
<name>Ana</name>
</author>
<published>2020-12-01T08:52:12+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=4302a75d82b9ac983cd89dd01c742c36777d921b'/>
<id>4302a75d82b9ac983cd89dd01c742c36777d921b</id>
<content type='text'>
Signed primitive integers defined on top of the existing unsigned ones
with two's complement.

The module Sint63 includes the theory of signed primitive integers that
differs from the unsigned case.

Additions to the kernel:
  les (signed &lt;=), lts (signed &lt;), compares (signed compare),
  divs (signed division), rems (signed remainder),
  asr (arithmetic shift right)
(The s suffix is not used when importing the Sint63 module.)

The printing and parsing of primitive ints was updated and the
int63_syntax_plugin was removed (we use Number Notation instead).

A primitive int is parsed / printed as unsigned or signed depending on
the scope. In the default (Set Printing All) case, it is printed in
hexadecimal.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Signed primitive integers defined on top of the existing unsigned ones
with two's complement.

The module Sint63 includes the theory of signed primitive integers that
differs from the unsigned case.

Additions to the kernel:
  les (signed &lt;=), lts (signed &lt;), compares (signed compare),
  divs (signed division), rems (signed remainder),
  asr (arithmetic shift right)
(The s suffix is not used when importing the Sint63 module.)

The printing and parsing of primitive ints was updated and the
int63_syntax_plugin was removed (we use Number Notation instead).

A primitive int is parsed / printed as unsigned or signed depending on
the scope. In the default (Set Printing All) case, it is printed in
hexadecimal.
</pre>
</div>
</content>
</entry>
<entry>
<title>Remove occurrences of Parray.reroot.</title>
<updated>2020-10-08T09:16:48+00:00</updated>
<author>
<name>Guillaume Melquiond</name>
</author>
<published>2020-08-31T06:52:05+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=e3764e1e857fce9b6d4cb018db676db3612c00a0'/>
<id>e3764e1e857fce9b6d4cb018db676db3612c00a0</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Primitive persistent arrays</title>
<updated>2020-07-06T09:22:43+00:00</updated>
<author>
<name>Maxime Dénès</name>
</author>
<published>2020-02-03T17:19:42+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=0ea2d0ff4ed84e1cc544c958b8f6e98f6ba2e9b6'/>
<id>0ea2d0ff4ed84e1cc544c958b8f6e98f6ba2e9b6</id>
<content type='text'>
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.

Co-authored-by: Benjamin Grégoire &lt;Benjamin.Gregoire@inria.fr&gt;
Co-authored-by: Gaëtan Gilbert &lt;gaetan.gilbert@skyskimmer.net&gt;
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.

Co-authored-by: Benjamin Grégoire &lt;Benjamin.Gregoire@inria.fr&gt;
Co-authored-by: Gaëtan Gilbert &lt;gaetan.gilbert@skyskimmer.net&gt;
</pre>
</div>
</content>
</entry>
<entry>
<title>Merge PR #12263: HaskellExtr: Add type annotations to Prelude.==</title>
<updated>2020-05-08T17:47:25+00:00</updated>
<author>
<name>Kazuhiko Sakaguchi</name>
</author>
<published>2020-05-08T17:47:25+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=343591ce6462543f1ffcdc1bfb0377042027ce12'/>
<id>343591ce6462543f1ffcdc1bfb0377042027ce12</id>
<content type='text'>
Reviewed-by: pi8027
Reviewed-by: zeldovich
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Reviewed-by: pi8027
Reviewed-by: zeldovich
</pre>
</div>
</content>
</entry>
<entry>
<title>Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpoints</title>
<updated>2020-05-08T10:25:16+00:00</updated>
<author>
<name>Pierre-Marie Pédrot</name>
</author>
<published>2020-05-08T10:25:16+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=8c13e5b6fe8ddb6bb78bfbe47a9ec190ec377872'/>
<id>8c13e5b6fe8ddb6bb78bfbe47a9ec190ec377872</id>
<content type='text'>
Ack-by: Zimmi48
Reviewed-by: ppedrot
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Ack-by: Zimmi48
Reviewed-by: ppedrot
</pre>
</div>
</content>
</entry>
<entry>
<title>HaskellExtr: Add type annotations to Prelude.==</title>
<updated>2020-05-06T16:18:30+00:00</updated>
<author>
<name>Jason Gross</name>
</author>
<published>2020-05-06T15:54:55+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=ffe7c11df6b6aac676498b09c63fc03db650ea8b'/>
<id>ffe7c11df6b6aac676498b09c63fc03db650ea8b</id>
<content type='text'>
Also `Export ExtrHaskellBasic` in `ExtrHaskellString`.

Fixes #12257
Fixes #12258
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Also `Export ExtrHaskellBasic` in `ExtrHaskellString`.

Fixes #12257
Fixes #12258
</pre>
</div>
</content>
</entry>
<entry>
<title>Fixing #11903: Fixpoints not truly recursive in standard library.</title>
<updated>2020-05-01T21:17:27+00:00</updated>
<author>
<name>Hugo Herbelin</name>
</author>
<published>2020-04-19T11:00:09+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=df8df4637dfb4106854554cc2ac94b4fdd565e80'/>
<id>df8df4637dfb4106854554cc2ac94b4fdd565e80</id>
<content type='text'>
There was also a non truly recursive in the doc.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
There was also a non truly recursive in the doc.
</pre>
</div>
</content>
</entry>
<entry>
<title>Quoting _CoqProject in a comment to avoid coqdoc to interpret it as emphasis.</title>
<updated>2020-04-05T13:44:18+00:00</updated>
<author>
<name>Hugo Herbelin</name>
</author>
<published>2020-04-05T13:14:25+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=f79e15086e9a6f002facd7411971a1f69beac46d'/>
<id>f79e15086e9a6f002facd7411971a1f69beac46d</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Update headers in the whole code base.</title>
<updated>2020-03-18T11:15:43+00:00</updated>
<author>
<name>Théo Zimmermann</name>
</author>
<published>2020-03-18T11:14:26+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=a99776e10e0b2198d2b811ad82631111fb450f8a'/>
<id>a99776e10e0b2198d2b811ad82631111fb450f8a</id>
<content type='text'>
Add headers to a few files which were missing them.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Add headers to a few files which were missing them.
</pre>
</div>
</content>
</entry>
</feed>
