aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
Commit message (Collapse)AuthorAge
* 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
|
* 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
|
* Default to /usr/bin/perlGravatar David Aspinall2002-06-08
|
* 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.
* Added some new tactic namesGravatar Pierre Courtieu2002-05-29
|
* WhitespaceGravatar David Aspinall2002-01-16
|
* Add Lemma to exclusion for coq-goal-command-p.Gravatar David Aspinall2001-09-24
|
* Coq/lego confusionGravatar David Aspinall2001-09-09
|
* Bug in new parsing for coq, mentionGravatar David Aspinall2001-09-09
|
* Add specific install instrs, rearrange.Gravatar David Aspinall2001-09-03
|
* 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
* fixed spelling;Gravatar Makarius Wenzel2000-11-27
|
* 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.
* Note about alternative path to perlGravatar David Aspinall2000-10-02
|
* added some comments in coq/todoGravatar Pierre Courtieu2000-09-29
|
* Make default path to perl be /usr/bin/perlGravatar David Aspinall2000-09-29
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 04:43:13 +0000