index
:
proof-general
master
Emacs interface for proof assistants
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Added some sections
David Aspinall
2002-06-18
*
News item for PG 3.4
David Aspinall
2002-06-18
*
Added the backtrack mechanism for sections. Seems to work.
Pierre Courtieu
2002-06-18
*
Added a function to inspect the prompt of Coq, in order to know if we
Pierre Courtieu
2002-06-18
*
Attempt at (alledgedly) more robust solution to find-and-forget.
David Aspinall
2002-06-18
*
Fix
David Aspinall
2002-06-18
*
Add more declarations
David Aspinall
2002-06-18
*
Test using proof-nesting-depth before calling Reset
David Aspinall
2002-06-18
*
Minor changes.
Pierre Courtieu
2002-06-14
*
Print and Check guess their argument from the region or the string
Pierre Courtieu
2002-06-14
*
Disable count-undos function, just use find-and-forget.
David Aspinall
2002-06-13
*
A nil setting of proof-kill-goal-command forces use of proof-find-and-forget ...
David Aspinall
2002-06-13
*
Docs
David Aspinall
2002-06-13
*
Experiment with showing real prover output for aborted proofs.
David Aspinall
2002-06-13
*
Revised find-and-forget function, which also works for count-undos.
David Aspinall
2002-06-12
*
More test cases, summary of situation.
David Aspinall
2002-06-12
*
Second variant of next-span, without doubly nested loop
David Aspinall
2002-06-12
*
Improve imp of next-span
David Aspinall
2002-06-12
*
Note of another bug
David Aspinall
2002-06-12
*
Test for find-and-forget using Back always instead of Reset.
David Aspinall
2002-06-12
*
Add test t4 for extra depth of nesting
David Aspinall
2002-06-12
*
Make hack for XEmacs 21.4 also work for later versions
David Aspinall
2002-06-12
*
Changed the CHANGES file for Coq.
Pierre Courtieu
2002-06-12
*
Nested proofs in Coq are well backtracked! I used the new field
Pierre Courtieu
2002-06-12
*
Adjust proof-nesting depth, add FIXME notes since not right yet
David Aspinall
2002-06-12
*
New files.
David Aspinall
2002-06-12
*
Add proof-nested-undo-regexp setting
David Aspinall
2002-06-12
*
Add nestedundos setting to span, and proof-nested-undo-regexp setting
David Aspinall
2002-06-12
*
Replace with example from Pierre
David Aspinall
2002-06-11
*
Only match saves for prover that supports nested proofs (restores old behavio...
David Aspinall
2002-06-11
*
Not important.
Pierre Courtieu
2002-06-11
*
CHANGE is cleaner in the Coq part! Not important.
Pierre Courtieu
2002-06-11
*
Added changes in CHANGE about my new customization variables
Pierre Courtieu
2002-06-11
*
Added the coq-user-... elisp customization variables to allow the user
Pierre Courtieu
2002-06-11
*
Remove proof-nested-goals-p setting
David Aspinall
2002-06-11
*
Improved proof-nesting-depth (not finished yet)
David Aspinall
2002-06-11
*
Fixed a bug of the new synchro code (coq-find-and-forget) in
Pierre Courtieu
2002-06-11
*
Add proof-nesting-depth, new implementation of span amalgamation in proof-don...
David Aspinall
2002-06-11
*
Set nested goals; include Lemma again in def of goal.
David Aspinall
2002-06-11
*
New files.
David Aspinall
2002-06-11
*
Mention not supporting E21
David Aspinall
2002-06-08
*
Updated.
David Aspinall
2002-06-08
*
Add install for isartags
David Aspinall
2002-06-08
*
Updated.
David Aspinall
2002-06-08
*
Fix bug in string syntax in isar-strip-terminators: did this work correctly b...
David Aspinall
2002-06-08
*
Clean up span.el loading; make compat with bbdb.el in FSF
David Aspinall
2002-06-08
*
Clean up span.el loading
David Aspinall
2002-06-08
*
Updated.
David Aspinall
2002-06-08
*
Updates
David Aspinall
2002-06-08
*
Remove duplicate
David Aspinall
2002-06-08
[next]