| Age | Commit message (Collapse) | Author |
|---|
|
proof-string-end-regexp, proof-comment-end, proof-comment-start,
and parentheses according to current syntax table;
renamed proof-commands-regexp to proof-indent-commands-regexp, which
is less confusing);
|
|
is less confusing);
|
|
proof-string-end-regexp;
|
|
|
|
closing a proof command;
|
|
|
|
more general qed schemes, such as Isabelle/Isar's nested proofs;
|
|
more general qed schemes, such as Isabelle/Isar's nested proofs;
|
|
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
|
|
|
|
|
|
|
|
end with a slash. Moreover, the closure proof-home-directory-fn is
added so that this value is not computed at compilation time.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
