aboutsummaryrefslogtreecommitdiff
path: root/coq
AgeCommit message (Collapse)Author
2002-06-19Finished updating the commands and tactic lists of coq-syntax.el.Pierre Courtieu
2002-06-19updated the lists of commands and tactics in coq-syntax.el.Pierre Courtieu
2002-06-19Use coq-proof-mode-p instead of nesting depth test. Attempt to track ↵David Aspinall
nesting depth (fails).
2002-06-19Clean up: remove count-undos, comments, tweak coq-proof-mode-p.David Aspinall
2002-06-18Removed lift-global stuff. coq-find-and-forget: only undo undoable tactics.David Aspinall
2002-06-18Added the backtrack mechanism for sections. Seems to work.Pierre Courtieu
2002-06-18Added a function to inspect the prompt of Coq, in order to know if wePierre Courtieu
are in proof-mode. Redundant with proof-nesting-depth.
2002-06-18Attempt at (alledgedly) more robust solution to find-and-forget.David Aspinall
2002-06-18Test using proof-nesting-depth before calling ResetDavid Aspinall
2002-06-14Minor changes.Pierre Courtieu
2002-06-14Print and Check guess their argument from the region or the stringPierre Courtieu
near the point.
2002-06-13Disable count-undos function, just use find-and-forget.David Aspinall
2002-06-12Revised find-and-forget function, which also works for count-undos.David Aspinall
2002-06-12Test for find-and-forget using Back always instead of Reset.David Aspinall
2002-06-12Nested proofs in Coq are well backtracked! I used the new fieldPierre Courtieu
'nestedundos created by David. Will change the CHANGE file accordingly.
2002-06-12Add proof-nested-undo-regexp settingDavid Aspinall
2002-06-11Added the coq-user-... elisp customization variables to allow the userPierre Courtieu
to defclare new commands and tactics: must typically be customized in .emacs.
2002-06-11Remove proof-nested-goals-p settingDavid Aspinall
2002-06-11Fixed a bug of the new synchro code (coq-find-and-forget) inPierre Courtieu
coq.el. Now do not count Tactics and unsaved goal commands for "Back".
2002-06-11Set nested goals; include Lemma again in def of goal.David Aspinall
2002-06-08Default to /usr/bin/perlDavid Aspinall
2002-05-29Made a negative test to compute the number of "Back n" inPierre Courtieu
coq-find-and-forget.
2002-05-29Modification of the coq-find-and-forget function, in order to use thePierre Courtieu
new "Back n." command of coq to make the syncronization better. Seems to work, need to test.
2002-05-29Added some new tactic namesPierre Courtieu
2002-01-16WhitespaceDavid Aspinall
2001-09-24Add Lemma to exclusion for coq-goal-command-p.David Aspinall
2001-09-09Coq/lego confusionDavid Aspinall
2001-09-09Bug in new parsing for coq, mentionDavid Aspinall
2001-09-03Add specific install instrs, rearrange.David Aspinall
2001-08-31Add auto-compile-vos experimental setting for automatic multiple files.David Aspinall
2001-08-28Added something in the doc about coq-version-is-V7, and made the setting ofPierre Courtieu
this variable more trustable with (concat coq-prog-name "-v").
2001-08-28Change of proof span type back to goalsaveDavid Aspinall
2001-04-10Modification of proof-script-command-end-regexp to allow commandsPierre Courtieu
ended by ".eof"
2001-03-20Added the config var proof-script-command-end-regexp fot coq V7.Pierre Courtieu
2001-02-26minor change in coq.el to allow to force version of coq, with variablePierre Courtieu
coq-version-is-V7
2000-12-20Experimental support for multiple file handling.David Aspinall
'goalsave -> 'proof
2000-11-27fixed spelling;Makarius Wenzel
2000-11-24Continuing Coq V7 compatibility work, Begin Silent -> Set Silent, etc...Pierre Courtieu
2000-11-24Add a little change to coq-find-and-forget to work betterPierre Courtieu
2000-11-23I am starting to make PG coqV7 compatible, I think the best is toPierre Courtieu
allow both V6 and V7 for a while. Theoretically, incompatibilities will not be numerous.
2000-10-02Note about alternative path to perlDavid Aspinall
2000-09-29added some comments in coq/todoPierre Courtieu
2000-09-29Make default path to perl be /usr/bin/perlDavid Aspinall
2000-09-29a little change in coq/x-symbol, nothingPierre Courtieu
2000-09-29A little work around for the bug of Coq concerning the restart thatPierre Courtieu
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).
2000-09-29Added Uncaught exception errors in coq-error-regexp.Pierre Courtieu
2000-09-27Updated from docDavid Aspinall
2000-08-26nothing important, I forgot to undo something before my last commit inPierre Courtieu
coq/x-symbol-coq.el
2000-08-26Some changes for undoing with coq, handle user-defined tactics, inPierre Courtieu
coq/coq-syntax.el and coq/coq.el.
2000-08-14enhancement of outline regexps for coq, now when hiding bodies, we seePierre Courtieu
completely definitions and theorems, but proof script are hidden (but can be blindly sent to the prover). Seems to work correctly.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 00:44:00 +0000