diff options
| author | Enrico Tassi | 2018-12-19 13:16:33 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-12-19 13:16:33 +0100 |
| commit | fb88eab3c323c752ad9d77649c77d5be9190d41e (patch) | |
| tree | 096ec23fea03461d62331cf7b38c91246477d7be | |
| parent | 235253d0a119cb97daa636646336d307bc96d5b7 (diff) | |
[doc] typo
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 66338d7f9f..92bd4dbd1d 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1617,7 +1617,7 @@ annotation: views are interpreted opening the ``ssripat`` scope. required to expose the top variable or assumption. ``>`` pops every variable occurring in the rest of the stack. - Type class instances are popped even if then don't occur + Type class instances are popped even if they don't occur in the rest of the stack. The tactic ``move=> >`` is equivalent to ``move=> ? ?`` on a goal such as:: |