<feed xmlns='http://www.w3.org/2005/Atom'>
<title>coq/COMPATIBILITY, branch master</title>
<subtitle>The formal proof system</subtitle>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/'/>
<entry>
<title>Archive COMPATIBILITY.</title>
<updated>2018-01-22T09:40:51+00:00</updated>
<author>
<name>Théo Zimmermann</name>
</author>
<published>2018-01-22T09:40:51+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=e8c32132796582b792f0b9a154fe568446526e95'/>
<id>e8c32132796582b792f0b9a154fe568446526e95</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Move the mention of the removal of Qed exporting at the right place.</title>
<updated>2018-01-22T09:37:46+00:00</updated>
<author>
<name>Théo Zimmermann</name>
</author>
<published>2018-01-22T09:37:46+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=a872ab42a338e0e9ccb5d1586b10fb961b66d425'/>
<id>a872ab42a338e0e9ccb5d1586b10fb961b66d425</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>[vernac] Remove `Qed exporting` syntax.</title>
<updated>2017-09-29T09:35:02+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2017-05-19T13:31:16+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=848bc5b5fc366ab5869a2836c5ad83ab4d0f2842'/>
<id>848bc5b5fc366ab5869a2836c5ad83ab4d0f2842</id>
<content type='text'>
We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.

Next step, understand why.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.

Next step, understand why.
</pre>
</div>
</content>
</entry>
<entry>
<title>A fix for #5390 (a useful error on used introduction names was masked).</title>
<updated>2017-05-17T21:38:26+00:00</updated>
<author>
<name>Hugo Herbelin</name>
</author>
<published>2017-03-12T12:18:42+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=741f3fab052b91eaec57f32b639ca722c3d8dc34'/>
<id>741f3fab052b91eaec57f32b639ca722c3d8dc34</id>
<content type='text'>
With the "apply in" introduction pattern, and the backtrack possibly
done in "apply" over the components of conjunctions
(descend_in_conjunctions), the reasons for failing might have
different sources.

We give priority to the detection of used names over other
(unification) errors so that an error there is not masked in the
backtracking made by descend_in_conjunctions.

Of course, the question of what best unification error to give in the
presence of backtracking is still open.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
With the "apply in" introduction pattern, and the backtrack possibly
done in "apply" over the components of conjunctions
(descend_in_conjunctions), the reasons for failing might have
different sources.

We give priority to the detection of used names over other
(unification) errors so that an error there is not masked in the
backtracking made by descend_in_conjunctions.

Of course, the question of what best unification error to give in the
presence of backtracking is still open.
</pre>
</div>
</content>
</entry>
<entry>
<title>Being more informative about the change of behavior of "subst".</title>
<updated>2016-09-29T15:35:37+00:00</updated>
<author>
<name>Hugo Herbelin</name>
</author>
<published>2016-09-29T15:33:47+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=14e47506ffabc43c25bf8da108abb6df78b803ad'/>
<id>14e47506ffabc43c25bf8da108abb6df78b803ad</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Update CHANGES and COMPATIBILITY</title>
<updated>2016-06-27T21:36:20+00:00</updated>
<author>
<name>Matthieu Sozeau</name>
</author>
<published>2016-06-21T17:06:30+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=5193311836394d3d18a0187a0d77657aa060b651'/>
<id>5193311836394d3d18a0187a0d77657aa060b651</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Merge branch 'v8.5'</title>
<updated>2016-05-20T09:39:59+00:00</updated>
<author>
<name>Pierre-Marie Pédrot</name>
</author>
<published>2016-05-20T09:39:59+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=dbe1c641164fc797edf0420f5f5a5e8b60b5a05a'/>
<id>dbe1c641164fc797edf0420f5f5a5e8b60b5a05a</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>More hints on how to fix compatibility issues.</title>
<updated>2016-05-14T18:19:16+00:00</updated>
<author>
<name>Hugo Herbelin</name>
</author>
<published>2016-04-28T19:17:23+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=1c26b08983f903538992eb1b5605c6ebe29fd175'/>
<id>1c26b08983f903538992eb1b5605c6ebe29fd175</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Merge branch 'v8.5'</title>
<updated>2015-03-23T12:10:34+00:00</updated>
<author>
<name>Pierre-Marie Pédrot</name>
</author>
<published>2015-03-23T12:10:34+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=224d3b0e8be9b6af8194389141c9508504cf887c'/>
<id>224d3b0e8be9b6af8194389141c9508504cf887c</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Qed export -&gt; Qed exporting</title>
<updated>2015-03-22T15:56:38+00:00</updated>
<author>
<name>Enrico Tassi</name>
</author>
<published>2015-03-22T15:56:38+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=4b1061a2e8cb93e6c1e3a1ef016e512eda9d0f64'/>
<id>4b1061a2e8cb93e6c1e3a1ef016e512eda9d0f64</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
</feed>
