changes.html

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
            "http://www.w3.org/TR/REC-html40/loose.dtd">
<HTML> <HEAD>
<TITLE>List of changes for Prooftree</TITLE>

<STYLE type="text/css">
h1 { background:#ffa500; color:#0048ff; text-align:center }
h2 { background:#ffa500; color:#0048ff; text-align:center }
h3 { color:#0048ff }
pre {
    border: 2pt red;
    overflow: auto;
    padding: 1em 1em;
	background : beige;
	color : black;
}
a img {
    border: 0;
}
</STYLE>

</HEAD>

<BODY>
<H1>List of Changes for Prooftree</H1>

<DL>
<!-- RECENT CHANGES START -->

<!-- 
 ! - <DT>XXXX-XX-XX
 ! - <DD>
 ! - <UL>
 ! - <LI>
 ! - <P></P></LI>
 ! - </UL>
  -->


<DT>2024-02-23: Prooftree 0.14 released
<DD>
<UL>
<LI>update Prooftree for Coq &GT;= 8.12
</LI>
<LI>this version of Prooftree requires Proof General &GT;= 4.6 or a
  development version with
  PR <a href="https://github.com/ProofGeneral/PG/pull/439">439</a>
  merged
</LI>
<LI>change communication protocol (version 4 now) to request sequent
  updates from Proof General asynchronously and explicit confirmation
  of proof completion
</LI>
<LI>accept unicode characters in names of existential variables
<P></P></LI>
</UL>

<!-- RECENT CHANGES END -->

<DT>2017-01-03: Prooftree 0.13 released
<DD>
<UL>
<LI>sequent history accessible in external sequent node windows
</LI>
<LI>new menu item <KBD>Show selected</KBD>
</LI>
<LI>improved configuration dialog
</LI>
<LI>support Coq 8.5 and 8.6
<P></P></LI>
</UL>


<DT>2013-05-17: Prooftree 0.12 released
<DD>
<UL>
<LI>bug fixes for clones
<P></P></LI>
</UL>


<DT>2013-01-21: Prooftree 0.11 released
<DD>
<UL>
<LI>incompatible protocol change: requires Proof General &GT;= 4.3pre130327
</LI>
<LI>support for bullets, braces and <KBD>Grab Existential
    Variables</KBD> of Coq 8.4
</LI>
<LI>New context menu items for retraction (undo), inserting proof
commands and proof scripts from subproofs
</LI>
<LI>several bug fixes and other small improvements
<P></P></LI>
</UL>


<DT>2012-05-14: Prooftree 0.10 released
<DD>
<UL>
<LI>bug fixes and internal changes
<P></P></LI>
</UL>

<DT>2012-01-04: Prooftree 0.9 released
<DD>
<UL>
<LI>fix case when some existential variables is instantiated by
the last proof command
<P></P></LI>
</UL>

<DT>2012-01-03: Prooftree 0.8 released
<DD>
<UL>
<LI>Works now with standard versions of Coq (&GT;= 8.4beta)
    and Proof General (current development version)
</LI>
<LI>Update <EM>all</EM> sequents when existential variables get
instantiated
</LI>
<LI>Display dependencies of existential variables
</LI>
<LI>various internal improvements
<P></P></LI>
</UL>

<DT>2011-11-01
<DD>
<UL>
<LI>Improved support for existential variables
<UL>
<LI>Dialog for marking introduction and instantiation points of
existential variables</LI>
<LI>Use a different color for branches that are proved but have
non-instantiated existential variables</LI>
<LI>display not instantiated existential variables in tool-tips,
sequent and proof command displays</LI>
</UL>
</LI>
<LI>several bug fixes
<P></P></LI>
</UL>

<DT>2011-10-04
<DD>
<UL>
<LI>in sync with Proof General version 4.1</LI>
<LI>several bug fixes
<P></P></LI>
</UL>

<DT>2011-08-11
<DD>
<UL>
<LI>User interface changes
    <UL>
    <LI>extra sequent and proof command windows on double click
        and shift click
    </LI>
    <LI>move proof tree by dragging with mouse button 1</LI>
    <LI>main menu with new help, about, exit items</LI>
    <LI>progress message between <KBD>Dismiss</KBD> and
           <KBD>Menu button</KBD>
        </LI>
    <LI>new Configuration dialog and support for user specific
           configurations</LI>
    <LI>tool tips show proof commands and sequents</LI>
    </UL>
</LI>
<LI>
man page added</LI>
<LI>several fixes and small changes<P></P>
</LI>
</UL>

<DT>2011-06-14
<DD>
<UL>
<LI>support starting prooftree in the middle of a proof
</LI>
<LI>display extra windows with the complete sequent text or the
complete proof command on mouse button 2
</LI>
<LI>the clone button yields a frozen copy of the proof tree 
</LI>
<LI>branches that are finished by a cheating tactic (such as
<KBD>admit</KBD> or <KBD>sorry</KBD>) are colored in red
</LI>
<LI>keep proof tree windows when retracting in a big step to a
point before the proof
<P></P></LI>
</UL>
<DT>2011-04-21
<DD>
<UL>
<LI><KBD>Show</KBD>, <KBD>Focus</KBD> and <KBD>Unfocus</KBD> work.
<P></P></LI>
</UL>

<DT>2011-04-20
<DD>
<UL>
<LI>Update existential variables when they are instantiated (as
far as possible)
</LI>
<LI>fix sequent window showing outdated text<P></P>
</LI>
</UL>

<DT>2011-04-18
<DD>
<UL>
<LI>first release
</LI>
</UL>


</DL>


<HR noshade size=2>
<FONT SIZE="-2">
last changed on 
<!-- hhmts start --> 2 Jan 2017
<!-- hhmts end -->
by <A HREF="/index.html.en">Hendrik</A>
</FONT></BODY> </HTML>