diff options
| author | Maxime Dénès | 2018-09-19 14:55:51 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-19 14:55:51 +0200 |
| commit | 007c084e3935eae639bb83c9dd9deefc1363d71d (patch) | |
| tree | 30306109d15b10d8de78ae7e583c5a1d48de4a55 /doc/sphinx/proof-engine | |
| parent | 6d74efabf11768ca1df3a2f3d5a65d25f7f95b01 (diff) | |
| parent | 12721b071cc76a463135ad74d572444b9d907b62 (diff) | |
Merge PR #7343: Add missing index entries.
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 70d46e034a..1fc267488c 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -717,6 +717,7 @@ Local definitions Local definitions can be done as follows: .. tacn:: let @ident__1 := @expr__1 {* with @ident__i := @expr__i} in @expr + :name: let ... := ... each :n:`@expr__i` is evaluated to :n:`v__i`, then, :n:`@expr` is evaluated by substituting :n:`v__i` to each occurrence of :n:`@ident__i`, for |