aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
1998-02-11prioritisedThomas Kleymann
1998-02-10*** empty log message ***Thomas Kleymann
1998-02-10added Dnf to lego-undoable-commands-regexpThomas Kleymann
1998-01-26X-Symbol version 4.45 betaDavid Aspinall
1998-01-26This commit was generated by cvs2git to track changes on a CVS vendorDavid Aspinall
1998-01-16Commented the code of proof.el and lego.el a bit. Made a minor changeDilip Sequiera
1998-01-15Added coq-shell-cdHealfdene Goguen
1998-01-15Updated method of defining proof-shell-cd to be consistent with otherHealfdene Goguen
1998-01-15One needed change for coq includedHealfdene Goguen
1998-01-12o added support for remote proof processesThomas Kleymann
1998-01-05improved fume supportThomas Kleymann
1998-01-05fixed a bug in the indenting functionsThomas Kleymann
1997-12-18*** empty log message ***Thomas Kleymann
1997-12-18o introduced proof-shell-handle-error-hook and bount it by default toThomas Kleymann
1997-11-26Noted bug in popup-eager-annotationDilip Sequiera
1997-11-26Added C-c C-s to run "Search" in Coq.Healfdene Goguen
1997-11-26A few new suggestionsHealfdene Goguen
1997-11-26Incorporated tms's suggestion for simplifying coq-font-lock-keywords-1Healfdene Goguen
1997-11-26o The response buffer focusses on the first goalThomas Kleymann
1997-11-26o simplified code:Thomas Kleymann
1997-11-26simplified code:Thomas 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-20Fixed outstanding things to be updated in Coq.Healfdene Goguen
1997-11-20Added lego-global-p as always false, but for consistency with Coq mode.Healfdene Goguen
1997-11-20Added coq-global-p for global declarations and definitions. These nowHealfdene Goguen
1997-11-18Added indentation for lego-mode.Dilip Sequiera
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-12Changed pbp-change-goal so that it only "Show"s the goal pointed at.Healfdene 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-11-06Assign new variable proof-goal-hyp-fn to lego-goal-hyp, which isHealfdene Goguen
1997-11-06Assign new variable proof-goal-hyp-fn to coq-goal-hyp, which advancesHealfdene Goguen
1997-11-06Updates to Coq fontlock tablesHealfdene 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-24New indentation for lego-count-undos (smile)Healfdene Goguen
1997-10-24Fixed coq-count-undos for commentsHealfdene Goguen
1997-10-24Changed order of "Inversion_clear" and "Inversion" so that former isHealfdene 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 coq-shell-prompt-pattern to reflect proof-idHealfdene Goguen
1997-10-17Added "Induction" as tacticHealfdene Goguen
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 Coq changes with main branch.Dilip Sequiera
1997-10-16Merged Coq changes onto main branchDilip Sequiera
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-05 02:16:40 +0000