Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Finished updating the commands and tactic lists of coq-syntax.el. | 2002-06-19 | |
| | |||
* | updated the lists of commands and tactics in coq-syntax.el. | 2002-06-19 | |
| | |||
* | Added the backtrack mechanism for sections. Seems to work. | 2002-06-18 | |
| | |||
* | Added a function to inspect the prompt of Coq, in order to know if we | 2002-06-18 | |
| | | | | are in proof-mode. Redundant with proof-nesting-depth. | ||
* | Added the coq-user-... elisp customization variables to allow the user | 2002-06-11 | |
| | | | | | to defclare new commands and tactics: must typically be customized in .emacs. | ||
* | Modification of the coq-find-and-forget function, in order to use the | 2002-05-29 | |
| | | | | | new "Back n." command of coq to make the syncronization better. Seems to work, need to test. | ||
* | Added some new tactic names | 2002-05-29 | |
| | |||
* | I am starting to make PG coqV7 compatible, I think the best is to | 2000-11-23 | |
| | | | | | allow both V6 and V7 for a while. Theoretically, incompatibilities will not be numerous. | ||
* | Added Uncaught exception errors in coq-error-regexp. | 2000-09-29 | |
| | |||
* | Some changes for undoing with coq, handle user-defined tactics, in | 2000-08-26 | |
| | | | | coq/coq-syntax.el and coq/coq.el. | ||
* | somme little changes to make undo work better | 2000-06-22 | |
| | |||
* | More decoration | 2000-04-07 | |
| | |||
* | Altered syntax a little bit so reset works for Section. | 2000-03-19 | |
| | |||
* | fixed some regexp via proof-anchor-regexp; | 1999-07-02 | |
| | |||
* | keywords of coq 6.3 | 1999-06-30 | |
| | |||
* | Hints Resolve | 1999-06-21 | |
| | |||
* | better syntax | 1999-06-16 | |
| | |||
* | Various updates. coq-end-Section now works properly. | 1999-06-14 | |
| | |||
* | More colors, more regexps, more keywords | 1999-06-09 | |
| | |||
* | several additions, as usual | 1999-05-17 | |
| | |||
* | OrElse -> Orelse | 1999-05-03 | |
| | |||
* | A few coloring tricks | 1999-04-20 | |
| | |||
* | Merged changes sent by Patrick Loiseleur. | 1999-04-07 | |
| | |||
* | Comments from Healf explaining need for coq-goal-command-p | 1999-02-22 | |
| | |||
* | Added note about removing proof-goal-command-p | 1998-11-12 | |
| | |||
* | fixed bug with font-lock face names | 1998-11-03 | |
| | |||
* | o added support for byte-compilation | 1998-11-01 | |
| | | | | | | | o removed hhg tags in todo o fixed font-lock for FSF Emacs 20.2 o ensured that goals buffer is updated for longer queues o fixed a bug in proof-universal-keys-only-mode | ||
* | Replaced remaining face defs with defface calls. | 1998-10-23 | |
| | | | | | Removed font-lock-<newface> with proof-<newface> so we know where things come from and won't break future font locks. | ||
* | changed maintainer information to lego@dcs and isabelle@dcs . | 1998-10-02 | |
| | |||
* | Updated maintainer tags to remove lego email address. | 1998-10-01 | |
| | |||
* | Removed history | 1998-09-23 | |
| | |||
* | Fixup branch number | 1998-09-09 | |
| | |||
* | Renamed for new subdirectory structure | 1998-09-03 | |