aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
Commit message (Collapse)AuthorAge
* little changes of menu/holes/abbrev in coq/pgGravatar Pierre Courtieu2004-02-26
|
* added menu entries to tactic menusGravatar Pierre Courtieu2004-02-19
|
* added submenus for command insertion for coq. menu uses abbrevGravatar Pierre Courtieu2004-02-19
| | | | expansion to build holes.
* added some lines in holes short doc. And some abbrevs for coq.Gravatar Pierre Courtieu2004-02-19
|
* added some menu entries for coq.Gravatar Pierre Courtieu2004-02-19
|
* Coq Abbrevs now make holes. I will add a menu with basic command.Gravatar Pierre Courtieu2004-02-18
|
* Avoid type error if coq program can't be found during startup.Gravatar David Aspinall2004-02-17
|
* Added some interface stuff:Gravatar Pierre Courtieu2004-02-11
| | | | | | | - an default coq abbrev file, loaded only if no abbrev table exists for coq; - some menu entries and shortcuts for abbrev; - a menu entry for "3 buffers view".
* little error in the syntax corrected.Gravatar Pierre Courtieu2004-02-11
|
* adapting to coq-8.0.Gravatar Pierre Courtieu2004-02-06
|
* Rever to simplest exampleGravatar David Aspinall2003-10-05
|
* Make find-and-forget robust for proverproc regionsGravatar David Aspinall2003-06-05
|
* Fix some compile errorsGravatar David Aspinall2003-02-24
|
* corrected a bug of pg/coq, the following line was not recognized as aGravatar Pierre Courtieu2003-02-20
| | | | | | | | | module start: Module M:T with Definition A:=u. I had to count the number of 'with' and ':=' to know if the last ':=' was a Module given explicitely (--> no module start) or only part of a 'with ...:=' (--> module start).
* Added documentation string to the variables coq-version-is-V6 (new),Gravatar Pierre Courtieu2003-02-16
| | | | coq-version-is-V7 and coq-version-is-V74.
* Fixes so that compile worksGravatar David Aspinall2003-02-15
|
* Added the keyword "Local :=" to the coq-goal-command-p function, likeGravatar Pierre Courtieu2003-02-12
| | | | Definition.
* little modif on the end-cammand regexp.Gravatar Pierre Courtieu2003-02-10
|
* little change to proof-script-command-end-regexp, again, to deal withGravatar Pierre Courtieu2003-02-06
| | | | coq-v6.2. In the next version we will remove support for coq < 7.0.
* Slight modification to proof-script-command-end-regexp in coq.el, toGravatar Pierre Courtieu2003-02-06
| | | | allow command at the end of the buffer.
* New setting for parse cmdend regexp.Gravatar David Aspinall2003-02-05
|
* Coq/pg: fixed a little bug with the "Print Hint" state preservingGravatar Pierre Courtieu2003-02-04
| | | | | | command, which must not be matched by the state changing command "Hint". I put "\\`Hint" in the keyword list, but I am not sure this is the best way.
* code cleaning + deals better with the new module system of Coq. DidGravatar Pierre Courtieu2003-02-03
| | | | not test the fsfemacs. Will do before release.
* Bug correction in the find-and-forget function for coq: in Coq v74, noGravatar Pierre Courtieu2003-01-30
| | | | | | prompt is return if an empty command is send ("\n"), so if the command is empty, we send proof-no-command (if not, backtracking state preserving command stays indefinitely in "proof process busy" state).
* Added a file for testing modules of coq (new version 7.4). Plus someGravatar Pierre Courtieu2003-01-29
| | | | modification to better backtrack modules.
* Fix hilight of Module Type?Gravatar David Aspinall2003-01-24
|
* removed some garbage printing in coq/Gravatar Pierre Courtieu2003-01-24
|
* Modifications for support of Coq-7.3.1+ and above (new module system).Gravatar Pierre Courtieu2003-01-24
|
* Updated.Gravatar David Aspinall2002-11-20
|
* Check on context menu doesn't seem useful.Gravatar David Aspinall2002-09-11
|
* Updated.Gravatar David Aspinall2002-09-11
|
* Improved implementation of zap-commas font lock behaviour, patch from Stefan ↵Gravatar David Aspinall2002-08-31
| | | | Monnier
* FormattingGravatar David Aspinall2002-08-30
|
* Layout/docstring improvements (based on patch from Stefan Monnier)Gravatar David Aspinall2002-08-29
|
* mPatch from Stefan Monnier [buffer-substring].Gravatar David Aspinall2002-08-29
|
* Patch for nested comments from Stefan Monnier.Gravatar David Aspinall2002-08-29
|
* Patch from Stefan Monnier for syntax highlighting.Gravatar David Aspinall2002-08-28
|
* Fix sloppy uses of message/concatGravatar David Aspinall2002-08-28
|
* Print ProofGravatar David Aspinall2002-08-16
|
* Finished the changing of names of config. variables (coq-user...).Gravatar Pierre Courtieu2002-07-27
|
* Changed once again the backtrack mechanism, it corresponds to what weGravatar Pierre Courtieu2002-07-26
| | | | agreed for some time ago. I am ok for a 3.4 now.
* Variable name change proof-comment-{start,end}-regexp -> ↵Gravatar David Aspinall2002-07-19
| | | | proof-script-comment-{start,end}-regexp.
* X-sym bugGravatar David Aspinall2002-07-18
|
* Add yet more settings X-Sym complains about.Gravatar David Aspinall2002-07-18
|
* Update versions/TODOGravatar David Aspinall2002-07-17
|
* Refactor several variable names; clean up, doc subterm markup and output ↵Gravatar David Aspinall2002-07-16
| | | | display.
* Finished updating the commands and tactic lists of coq-syntax.el.Gravatar Pierre Courtieu2002-06-19
|
* updated the lists of commands and tactics in coq-syntax.el.Gravatar Pierre Courtieu2002-06-19
|
* Use coq-proof-mode-p instead of nesting depth test. Attempt to track ↵Gravatar David Aspinall2002-06-19
| | | | nesting depth (fails).
* Clean up: remove count-undos, comments, tweak coq-proof-mode-p.Gravatar David Aspinall2002-06-19
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 15:37:27 +0000