aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq.el
Commit message (Collapse)AuthorAge
* 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
| | | | are in proof-mode. Redundant with proof-nesting-depth.
* 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
| | | | near the point.
* 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
|
* Nested proofs in Coq are well backtracked! I used the new fieldGravatar Pierre Courtieu2002-06-12
| | | | | 'nestedundos created by David. Will change the CHANGE file accordingly.
* Add proof-nested-undo-regexp settingGravatar David Aspinall2002-06-12
|
* Added the coq-user-... elisp customization variables to allow the userGravatar Pierre Courtieu2002-06-11
| | | | | to defclare new commands and tactics: must typically be customized in .emacs.
* Remove proof-nested-goals-p settingGravatar David Aspinall2002-06-11
|
* Fixed a bug of the new synchro code (coq-find-and-forget) inGravatar Pierre Courtieu2002-06-11
| | | | coq.el. Now do not count Tactics and unsaved goal commands for "Back".
* Set nested goals; include Lemma again in def of goal.Gravatar David Aspinall2002-06-11
|
* Made a negative test to compute the number of "Back n" inGravatar Pierre Courtieu2002-05-29
| | | | coq-find-and-forget.
* Modification of the coq-find-and-forget function, in order to use theGravatar Pierre Courtieu2002-05-29
| | | | | new "Back n." command of coq to make the syncronization better. Seems to work, need to test.
* Add Lemma to exclusion for coq-goal-command-p.Gravatar David Aspinall2001-09-24
|
* Add auto-compile-vos experimental setting for automatic multiple files.Gravatar David Aspinall2001-08-31
|
* Added something in the doc about coq-version-is-V7, and made the setting ofGravatar Pierre Courtieu2001-08-28
| | | | this variable more trustable with (concat coq-prog-name "-v").
* Change of proof span type back to goalsaveGravatar David Aspinall2001-08-28
|
* Modification of proof-script-command-end-regexp to allow commandsGravatar Pierre Courtieu2001-04-10
| | | | ended by ".eof"
* Added the config var proof-script-command-end-regexp fot coq V7.Gravatar Pierre Courtieu2001-03-20
|
* minor change in coq.el to allow to force version of coq, with variableGravatar Pierre Courtieu2001-02-26
| | | | coq-version-is-V7
* Experimental support for multiple file handling.Gravatar David Aspinall2000-12-20
| | | | 'goalsave -> 'proof
* Continuing Coq V7 compatibility work, Begin Silent -> Set Silent, etc...Gravatar Pierre Courtieu2000-11-24
|
* Add a little change to coq-find-and-forget to work betterGravatar Pierre Courtieu2000-11-24
|
* I am starting to make PG coqV7 compatible, I think the best is toGravatar Pierre Courtieu2000-11-23
| | | | | allow both V6 and V7 for a while. Theoretically, incompatibilities will not be numerous.
* A little work around for the bug of Coq concerning the restart thatGravatar Pierre Courtieu2000-09-29
| | | | | | | uses Reset Initial which doesn't reset the Implicit Arguments flag to Off (this is the bug), I added the good command to the coq reset command, this has to be backtracked when V7 will be done (the bug is already corrected in V7).
* Added Uncaught exception errors in coq-error-regexp.Gravatar Pierre Courtieu2000-09-29
|
* Some changes for undoing with coq, handle user-defined tactics, inGravatar Pierre Courtieu2000-08-26
| | | | coq/coq-syntax.el and coq/coq.el.
* enhancement of outline regexps for coq, now when hiding bodies, we seeGravatar Pierre Courtieu2000-08-14
| | | | | completely definitions and theorems, but proof script are hidden (but can be blindly sent to the prover). Seems to work correctly.
* Removed some (hopefully redundant) requires.Gravatar David Aspinall2000-07-16
|
* somme little changes to make undo work betterGravatar Pierre Courtieu2000-06-22
|
* basic setup for new indentation code;Gravatar Makarius Wenzel2000-06-08
|
* Added 3 entries in the Coq menu: Print Check and HintsGravatar Pierre Courtieu2000-06-02
|
* Removed time setting, added proof-assistant-settings-cmd to init string, but ↵Gravatar David Aspinall2000-06-01
| | | | commented out
* Added a couple of settings for CoqGravatar David Aspinall2000-06-01
|
* Removed use of proof-terminal-string, added explicit terminators everywhere.Gravatar David Aspinall2000-05-29
|
* Changed keybindings for coq specific functionsGravatar David Aspinall2000-05-29
|
* proof-defass-default -> defpgdefaultGravatar David Aspinall2000-05-26
|
* debugging coq menu for old Xemacs compatibility, David said he will do thisGravatar Pierre Courtieu2000-05-16
| | | | for other provers (already done ?).
* Changes and compatibility fixes for specific menu/keybindings.Gravatar David Aspinall2000-05-11
|
* Added proof-assistant-keymap and commands for defining insert keys.Gravatar David Aspinall2000-05-02
|
* Added specific menu for Coq.Gravatar David Aspinall2000-05-01
|
* pbp-mode -> goals-modeGravatar David Aspinall2000-04-07
|
* Fixed up proof-shell-proof-completed mess nicely.Gravatar David Aspinall2000-04-07
|
* 3.1 not 3.2 changeGravatar David Aspinall2000-03-24
|
* Removed spurious requiresGravatar David Aspinall2000-03-24
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 01:56:02 +0000