diff options
| author | Maxime Dénès | 2018-04-16 21:26:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-04-16 23:29:00 +0200 |
| commit | a3ee82e80083fff971e382f52d9295fda2210e2d (patch) | |
| tree | c33240b821d78fb63bd0a3bb0a8d2bf17507f6c2 /doc/sphinx/addendum/program.rst | |
| parent | abd6bbd90753fd98355e551d8dc8ecfd07494639 (diff) | |
[Sphinx] Clean-up 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, |