aboutsummaryrefslogtreecommitdiff
path: root/proof.el
AgeCommit message (Expand)Author
1998-03-25added support for etags at generic proof levelThomas Kleymann
1998-03-24*** empty log message ***Thomas Kleymann
1998-01-16Commented the code of proof.el and lego.el a bit. Made a minor changeDilip Sequiera
1998-01-15Updated method of defining proof-shell-cd to be consistent with otherHealfdene Goguen
1998-01-12o added support for remote proof processesThomas Kleymann
1998-01-05improved fume supportThomas Kleymann
1997-12-18o introduced proof-shell-handle-error-hook and bount it by default toThomas Kleymann
1997-11-26o The response buffer focusses on the first goalThomas Kleymann
1997-11-24Added proof-execute-minibuffer-cmd and scripting minor mode.Dilip Sequiera
1997-11-20Added proof-global-p to test whether a 'vanilla should be lifted aboveHealfdene Goguen
1997-11-17Added some magic commands: proof-frob-locked-end, proof-try-command,Dilip Sequiera
1997-11-13Includes commented code for Coq version of extent protocolHealfdene Goguen
1997-11-10Started modifications for emacs19 port.Dilip Sequiera
1997-11-10Put in a workaround for a strange bug in comint which was finding a bunchDilip Sequiera
1997-11-06Parameterize by proof-goal-hyp-fn in pbp-make-top-extent, to handleHealfdene Goguen
1997-10-31o implented proof-find-next-terminator available via C-c C-eThomas Kleymann
1997-10-30Updates for coq, including:Healfdene Goguen
1997-10-24Updated comment about extent typesHealfdene Goguen
1997-10-22Updated proof-segment-up-to to take ""'s into accountHealfdene Goguen
1997-10-17proof-active-terminator inside comment case fixed. Also maybe theDilip Sequiera
1997-10-17fixed a bug in proof-process-active-terminator. Notice that it stillThomas Kleymann
1997-10-16Figured out display tables.Dilip Sequiera
1997-10-16merged script management (1.10.2.18) with main branchThomas Kleymann
1997-10-14proof-process-active-terminator is now an extension ofThomas Kleymann
1997-10-13put script-management branch back on main branchThomas Kleymann
1996-12-03Invisible pbp command handlingDilip Sequiera
1996-12-03A few small fixes to deal with performance problems.Dilip Sequiera
1996-11-22*** empty log message ***Thomas Kleymann
1996-11-21*** empty log message ***Thomas Kleymann
1996-11-05Bug with semicolon minor mode near-fixedDilip Sequiera
1996-11-05fixed bug in ids-to-regexp and improved regular expression for fontifying LEGOThomas Kleymann
1996-11-01improved font-lock customisation for LEGOThomas Kleymann
1996-10-29Fixed some bugs. Doubtless introduced others.Dilip Sequiera
1996-10-25added proof-find-end-of-commandThomas Kleymann
1996-10-24Emacs mode for legolego