aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
Commit message (Collapse)AuthorAge
...
* Error highlighting in coq only when scripting (not when sendingGravatar Pierre Courtieu2006-10-23
| | | | command invisibly).
* Fix for coq-utf-safe.Gravatar Pierre Courtieu2006-10-06
|
* utf safe coq mode is not linked to proof-shell-unicode, as unicode isGravatar Pierre Courtieu2006-09-29
| | | | not well handle by xemacs.
* adapting to proof-shell-unicode. Coq has not been adapted to theGravatar Pierre Courtieu2006-09-29
| | | | -emacs-U option.
* Simplified prompt regexp for coq, preparing new prompt delimitersGravatar Pierre Courtieu2006-09-29
| | | | <prompt> and </prompt>.
* fixed a bug with wakeup char for coq.Gravatar Pierre Courtieu2006-09-29
|
* Added \x6 as a possible wakeup char for coq. For the moment thisGravatar Pierre Courtieu2006-09-25
| | | | | special char is used when the -emacs-U is used (with or instead of -emacs) in cvs version of coq of today 25/9/2006.
* typo in coq-indent.Gravatar Pierre Courtieu2006-09-15
|
* fixed a typo in last correction.Gravatar Pierre Courtieu2006-09-15
|
* fix a bug with error highlighting. Not sure it is ok but seems toGravatar Pierre Courtieu2006-09-14
| | | | work.
* fixed a bug from Stefan Monnier.Gravatar Pierre Courtieu2006-09-14
|
* cleaning from Stefan Monnier.Gravatar Pierre Courtieu2006-09-13
|
* cleaning from Stefan Monnier.Gravatar Pierre Courtieu2006-09-13
|
* Fixed nested comment support for scripting, in xemacs (worked alreadyGravatar Pierre Courtieu2006-09-08
| | | | on GNU Emacs). Instanciated proof-parse-function for that...
* Updated.Gravatar David Aspinall2006-09-07
|
* Updated CHANGES.Gravatar Pierre Courtieu2006-09-07
|
* Added Goal as a goal starter in syntax db.Gravatar Pierre Courtieu2006-09-07
|
* updating changes in coq/CHANGES.Gravatar Pierre Courtieu2006-09-06
|
* Making error highlighting more robust (for both emacsen) and use aGravatar Pierre Courtieu2006-09-06
| | | | span instead of region.
* Error highliting in coq now worksGravatar Pierre Courtieu2006-09-05
|
* still experimenting error highlitingGravatar Pierre Courtieu2006-09-05
|
* Experimenting highlighting the error from coqtop errorGravatar Pierre Courtieu2006-09-05
| | | | | message. Function work but proof-shell-handle-error-or-interrupt-hook does not allow to activate the region...
* Trying to mae indentation aware of nested comments (to be simplifiedGravatar Pierre Courtieu2006-09-04
| | | | | when xemacs will deal with nested comments). Seems to work, a bit slow.
* fixes again in syntax databases.Gravatar Pierre Courtieu2006-08-25
|
* fix in syntax tables.Gravatar Pierre Courtieu2006-08-25
|
* Small fixes on syntax tables.Gravatar Pierre Courtieu2006-08-25
|
* Adding commentsGravatar Pierre Courtieu2006-08-25
|
* fix coq/CHANGESGravatar Pierre Courtieu2006-08-25
|
* Small fixes.Gravatar Pierre Courtieu2006-08-25
|
* Changed default coq version (8.1)Gravatar Pierre Courtieu2006-08-25
| | | | Small fixes in docstrings.
* added a CHANGES file for coq directoryGravatar Pierre Courtieu2006-08-25
| | | | filled it
* Fixed a small bug in indentation of coq.Gravatar Pierre Courtieu2006-08-25
| | | | Fixed behavior for making abbrev table (don't if it already exists).
* Changed state-preserving check for coq.Gravatar Pierre Courtieu2006-08-24
|
* changed coq bqcktracking to avoid doing backtrack x y z when x y and zGravatar Pierre Courtieu2006-08-24
| | | | | | are identical to current ones. This is because Backtrack x y z is sometimes slow even in such cases. Hopefully this won't break synchronization.
* fixing a bug introduced lately (coq-save-command-p *needs* two argsGravatar Pierre Courtieu2006-08-24
| | | | beacause proof-save-command-p needs is so defined).
* Fixed indentation and font-lock for coq. Better, faster.Gravatar Pierre Courtieu2006-08-23
|
* Coq indentation small fixes.Gravatar Pierre Courtieu2006-08-23
|
* fsf emacs compatibilty for symbol-at-point.Gravatar Pierre Courtieu2006-08-23
|
* Cleaning in coq and lib, fixed licenses and docstrings.Gravatar Pierre Courtieu2006-08-23
| | | | Added one or two details to docstring of generic variables.
* Finished making functions over big tables non recursive. Works withGravatar Pierre Courtieu2006-08-23
| | | | emacs.
* Making non recursive functions to make fsf emacs happy, not yet finished.Gravatar Pierre Courtieu2006-08-22
|
* Big redesign of the coq syntax defintion, centralization in big tablesGravatar Pierre Courtieu2006-08-22
| | | | like coq-commands-db.
* Menus redesign, new interactive tactics/commands/termsGravatar Pierre Courtieu2006-08-21
| | | | insertion. Great!
* Started the coq-insert-tactic.Gravatar Pierre Courtieu2006-08-21
|
* Moved the coq local variables tools in a separate file and made itGravatar Pierre Courtieu2006-08-17
| | | | simpler.
* continue on the support for local variables list semi-automaticGravatar Pierre Courtieu2006-08-17
| | | | | insertion. I put a new file in lib with basic tools for file variables lists.
* Added entries in coq menu, rearranged coq menu.Gravatar Pierre Courtieu2006-08-16
| | | | | Also added semi-automated setting of local file variables (*** Local Variables ***) coq-prog-name and coq-prog-args.
* fixed a bug with scripting with coq v8.0.Gravatar Pierre Courtieu2006-07-20
|
* removed debug messages from indentation code.Gravatar Pierre Courtieu2006-07-04
|
* fix the bug for coq indetation of two consecutive comments. Code isGravatar Pierre Courtieu2006-07-04
| | | | | ugly, should take the code given by Stefan Monnier and adapt it (it does not indent everything as is).
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 15:10:01 +0000