aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
Commit message (Expand)AuthorAge
* 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
* Added documentation string to the variables coq-version-is-V6 (new),Gravatar Pierre Courtieu2003-02-16
* 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
* 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
* Slight modification to proof-script-command-end-regexp in coq.el, toGravatar Pierre Courtieu2003-02-06
* 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
* code cleaning + deals better with the new module system of Coq. DidGravatar Pierre Courtieu2003-02-03
* Bug correction in the find-and-forget function for coq: in Coq v74, noGravatar Pierre Courtieu2003-01-30
* Added a file for testing modules of coq (new version 7.4). Plus someGravatar Pierre Courtieu2003-01-29
* 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
* 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
* Variable name change proof-comment-{start,end}-regexp -> proof-script-comment...Gravatar David Aspinall2002-07-19
* 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 disp...Gravatar David Aspinall2002-07-16
* 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 nesting...Gravatar David Aspinall2002-06-19
* Clean up: remove count-undos, comments, tweak coq-proof-mode-p.Gravatar David Aspinall2002-06-19
* Removed lift-global stuff. coq-find-and-forget: only undo undoable tactics.Gravatar David Aspinall2002-06-18
* Added the backtrack mechanism for sections. Seems to work.Gravatar Pierre Courtieu2002-06-18
* Added a function to inspect the prompt of Coq, in order to know if weGravatar Pierre Courtieu2002-06-18
* Attempt at (alledgedly) more robust solution to find-and-forget.Gravatar David Aspinall2002-06-18
* Test using proof-nesting-depth before calling ResetGravatar David Aspinall2002-06-18
* Minor changes.Gravatar Pierre Courtieu2002-06-14
* Print and Check guess their argument from the region or the stringGravatar Pierre Courtieu2002-06-14
* Disable count-undos function, just use find-and-forget.Gravatar David Aspinall2002-06-13
* Revised find-and-forget function, which also works for count-undos.Gravatar David Aspinall2002-06-12
* Test for find-and-forget using Back always instead of Reset.Gravatar David Aspinall2002-06-12