List of Changes for Prooftree

2024-02-23: Prooftree 0.14 released

• update Prooftree for Coq >= 8.12
• this version of Prooftree requires Proof General >= 4.6 or a development version with PR 439 merged
• change communication protocol (version 4 now) to request sequent updates from Proof General asynchronously and explicit confirmation of proof completion
• accept unicode characters in names of existential variables

2017-01-03: Prooftree 0.13 released

• sequent history accessible in external sequent node windows
• new menu item Show selected
• improved configuration dialog
• support Coq 8.5 and 8.6

2013-05-17: Prooftree 0.12 released

• bug fixes for clones

2013-01-21: Prooftree 0.11 released

• incompatible protocol change: requires Proof General >= 4.3pre130327
• support for bullets, braces and Grab Existential Variables of Coq 8.4
• New context menu items for retraction (undo), inserting proof commands and proof scripts from subproofs
• several bug fixes and other small improvements

2012-05-14: Prooftree 0.10 released

• bug fixes and internal changes

2012-01-04: Prooftree 0.9 released

• fix case when some existential variables is instantiated by the last proof command

2012-01-03: Prooftree 0.8 released

• Works now with standard versions of Coq (>= 8.4beta) and Proof General (current development version)
• Update all sequents when existential variables get instantiated
• Display dependencies of existential variables
• various internal improvements

2011-11-01

• Improved support for existential variables
  • Dialog for marking introduction and instantiation points of existential variables
  • Use a different color for branches that are proved but have non-instantiated existential variables
  • display not instantiated existential variables in tool-tips, sequent and proof command displays
• several bug fixes

2011-10-04

• in sync with Proof General version 4.1
• several bug fixes

2011-08-11

• User interface changes
  • extra sequent and proof command windows on double click and shift click
  • move proof tree by dragging with mouse button 1
  • main menu with new help, about, exit items
  • progress message between Dismiss and Menu button
  • new Configuration dialog and support for user specific configurations
  • tool tips show proof commands and sequents
• man page added
• several fixes and small changes

2011-06-14

• support starting prooftree in the middle of a proof
• display extra windows with the complete sequent text or the complete proof command on mouse button 2
• the clone button yields a frozen copy of the proof tree
• branches that are finished by a cheating tactic (such as admit or sorry) are colored in red
• keep proof tree windows when retracting in a big step to a point before the proof

2011-04-21

• Show, Focus and Unfocus work.

2011-04-20

• Update existential variables when they are instantiated (as far as possible)
• fix sequent window showing outdated text

2011-04-18

• first release