diff options
| author | Vincent Laporte | 2018-10-24 11:38:09 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-10-24 11:54:31 +0000 |
| commit | 35a2d07115cb1b41c5a32f8abd3608e37eae32dc (patch) | |
| tree | 4ff7da76a322a083ff2710d506b38613b29fd404 | |
| parent | ac613856324317543828632eaeb77ccb575c2f8f (diff) | |
[Manual] 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 70d17b1915..4fc3c24e89 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -4920,7 +4920,7 @@ which produces the converse implication. In both cases, the two first Prop arguments are implicit. If ``term`` is an instance of the ``reflect`` predicate, then ``A`` will be one -of the defined view hints for the ``reflec``t predicate, which are by +of the defined view hints for the ``reflect`` predicate, which are by default the ones present in the file ``ssrbool.v``. These hints are not only used for choosing the appropriate direction of the translation, but they also allow complex transformation, involving negations. |