diff options
| author | Maxime Dénès | 2018-04-16 23:30:05 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-04-16 23:30:05 +0200 |
| commit | 27b848dc388633ebfc58be8e7578069a3121dc27 (patch) | |
| tree | 3c191602e4899a50b0e9d99c5b3c2aa0e5a47312 /doc/sphinx/addendum/program.rst | |
| parent | eb9c9df833ae908a6e0e22260439fc263aed2b6b (diff) | |
| parent | a3ee82e80083fff971e382f52d9295fda2210e2d (diff) | |
Merge PR #7270: Sphinx doc fix indices
Diffstat (limited to 'doc/sphinx/addendum/program.rst')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 1c3fdeb430..be30d1bc4a 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -151,7 +151,7 @@ Program Definition obligations. Once solved using the commands shown below, it binds the final |Coq| term to the name ``ident`` in the environment. - .. exn:: ident already exists + .. exn:: @ident already exists (Program Definition) .. cmdv:: Program Definition @ident : @type := @term @@ -276,6 +276,7 @@ obligations (e.g. when defining mutually recursive blocks). The optional tactic is replaced by the default one if not specified. .. cmd:: {? Local|Global} Obligation Tactic := @tactic + :name: Obligation Tactic Sets the default obligation solving tactic applied to all obligations automatically, whether to solve them or when starting to prove one, |