| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1998-09-03 | Renamed for new subdirectory structure | David Aspinall | |
| 1998-09-03 | minor modifications | Thomas Kleymann | |
| 1998-09-03 | Dead code. | David Aspinall | |
| 1998-09-03 | Removed dead code | David Aspinall | |
| 1998-08-11 | Renamed <file>-fontlock to <file>-syntax | David Aspinall | |
| 1998-06-10 | Added coq-init-syntax-table as function to initialize syntax entries | Healfdene Goguen | |
| particular to coq. Changed proof-ctxt-string to "Print All". Call coq-init-syntax-table from coq-shell-mode-config. This was necessary to get prompts with "'"s in them (coming from goals with same) recognized. | |||
| 1998-06-03 | Added '?'s before single characters in define-keys for emacs19, at | Healfdene Goguen | |
| Pascal Brisset's suggestion. | |||
| 1998-06-03 | Added definition of proof-commands-regexp for coq | Healfdene Goguen | |
| 1998-06-02 | Generalized proof-retract-target, now parameterized by | Healfdene Goguen | |
| proof-count-undos and proof-find-and-forget. Generalized proof-shell-analyse-structure, introduced variable proof-analyse-using-stack. Generalized proof menu plus ancillary functions. Generalized proof-mode-version-string. Moved various comments into documentation string. | |||
| 1998-05-23 | improved support for Info | Thomas Kleymann | |
| o employed `Info-default-directory-list' rather than `Info-directory-list' so that code also works for Emacs 19.34 o setting of `Info-default-directory-list' now at proof level | |||
| 1998-05-22 | Correct path for coq-prog-name and coq-tags. | Healfdene Goguen | |
| 1998-05-15 | Changed variable names [s]ext to span. | Healfdene Goguen | |
| Fixed coq-find-and-forget pattern for declarations and definitions following Pascal Brisset's suggestion. | |||
| 1998-05-14 | Changes to indentation code: | Healfdene Goguen | |
| Changed "case" to "Case". Added "CoInductive". | |||
| 1998-05-12 | Added hook `coq-shell-init-hook', for `proof-shell-insert-hook'. | Healfdene Goguen | |
| This initializes undo limit and changes directory to that associated with buffer. This is because Coq has a command line option to run with emacs mode. | |||
| 1998-05-08 | Made separated indentation more elegant. | Healfdene Goguen | |
| Fixed bug with Inductive. Added CoInductive. | |||
| 1998-05-08 | Merged indentation code for LEGO and Coq into proof.el. | Healfdene Goguen | |
| 1998-05-06 | Removed default instantiation of undo limit to 100. | Healfdene Goguen | |
| 1998-05-06 | Added coq-info-dir so that script-management.info can be hard-coded. | Healfdene Goguen | |
| 1998-05-05 | Made updates to fix problem with Definition, which couldn't be | Healfdene Goguen | |
| used with proof scripts. Removed some useless declarations. Removed Abort from menu. Now Reset's if user undoes to beginning of proof. Added command to increase undo limit for Coq, and set default to 100. | |||
| 1998-03-25 | added support for etags at generic proof level | Thomas Kleymann | |
| 1998-01-15 | Added coq-shell-cd | Healfdene Goguen | |
| Some new fontlocks | |||
| 1997-11-26 | Added C-c C-s to run "Search" in Coq. | Healfdene Goguen | |
| Moved coq-goal-with-hole-regexp etc to coq-fontlock. Removed various superfluous definitions for COQPATH etc. | |||
| 1997-11-24 | Added proof-execute-minibuffer-cmd and scripting minor mode. | Dilip Sequiera | |
| 1997-11-20 | Added coq-global-p for global declarations and definitions. These now | Healfdene Goguen | |
| get lifted in the same way as lemmas. Changed [meta (control i)] to [meta tab] in key definition. Changed menu, and made help in menu refer to info mode. | |||
| 1997-11-17 | Added some magic commands: proof-frob-locked-end, proof-try-command, | Dilip Sequiera | |
| proof-interrupt-process. Added moving nested lemmas above goal for coq. Changed the key mapping for assert-until-point to C-c RET. | |||
| 1997-11-12 | Changed pbp-change-goal so that it only "Show"s the goal pointed at. | Healfdene Goguen | |
| 1997-11-06 | Assign new variable proof-goal-hyp-fn to coq-goal-hyp, which advances | Healfdene Goguen | |
| over coq-goal-regexp to pick up goal for pbp | |||
| 1997-10-30 | Updates for coq, including: | Healfdene Goguen | |
| * pbp-goal-command and pbp-hyp-command use proof-terminal-string * updates to keywords * fix for goal regexp | |||
| 1997-10-24 | Fixed coq-count-undos for comments | Healfdene Goguen | |
| 1997-10-17 | Fixed coq-shell-prompt-pattern to reflect proof-id | Healfdene Goguen | |
| Changed ";" to "." in coq-save-with-hole-regexp New modifications to syntax table to reflect actual use of symbols in Coq | |||
| 1997-10-16 | Merged Coq changes with main branch. | Dilip Sequiera | |
| 1997-10-16 | Merged Coq changes onto main branch | Dilip Sequiera | |
| 1997-10-13 | *** empty log message *** | Thomas Kleymann | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |