| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Corrected name of Texinfo and other comments.
|
|
|
|
|
