diff options
| author | Théo Zimmermann | 2019-10-04 20:02:35 +0200 |
|---|---|---|
| committer | GitHub | 2019-10-04 20:02:35 +0200 |
| commit | dc8a3cff5ff76735ed6a91145535678322806db9 (patch) | |
| tree | 53f929fa09973c91b56813817071131a41f280a7 | |
| parent | 2cff572ecea5846b23370c6912ff488bb099e761 (diff) | |
Improve language.
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index b7eb06662d..46c349f3e7 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3071,7 +3071,7 @@ the conversion in hypotheses :n:`{+ @ident}`. This tactic evaluates the goal using the optimized call-by-value evaluation bytecode-based virtual machine described in :cite:`CompiledStrongReduction`. This algorithm is dramatically more efficient than the algorithm used for the - :tacn:`cbv` tactic, but it cannot be fine-tuned. It is specially interesting for + :tacn:`cbv` tactic, but it cannot be fine-tuned. It is especially interesting for full evaluation of algebraic objects. This includes the case of reflection-based tactics. |