| Age | Commit message (Collapse) | Author |
|---|
|
proof-shell-eager-annotation-start-length.
|
|
|
|
|
|
|
|
|
|
Patch for more flexible handling of closing goal...save regions
after proof has been completed.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
by my name Pierre Courtieu.
|
|
|
|
Added proof-unnamed-theorem-name.
|
|
buffer. Added a version of it to proof-activate-scripting-hook.
Removed cd from initialization sequence.
Changed prover specifics accordingly.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
directory.
|
|
Would be nice to add more theorems to compare scripts in different
systems.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
is less confusing);
|
|
|
|
the function coq-guess-command-line in the coq part. Every prover
should have the functon *-guess-command-line that uses, for example,
the output of "make -n" to guess the correct command line options of
the prover.
Patrick
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
