diff options
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 25 |
1 files changed, 21 insertions, 4 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 7eef504ea9..081fef07b9 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3307,12 +3307,29 @@ the conversion in hypotheses :n:`{+ @ident}`. :name: fold This tactic applies to any goal. The term :n:`@term` is reduced using the - ``red`` tactic. Every occurrence of the resulting :n:`@term` in the goal is - then replaced by :n:`@term`. + :tacn:`red` tactic. Every occurrence of the resulting :n:`@term` in the goal is + then replaced by :n:`@term`. This tactic is particularly useful when a fixpoint + definition has been wrongfully unfolded, making the goal very hard to read. + On the other hand, when an unfolded function applied to its argument has been + reduced, the :tacn:`fold` tactic won't do anything. -.. tacv:: fold {+ @term} + .. example:: + + .. coqtop:: all + + Goal ~0=0. + unfold not. + Fail progress fold not. + pattern (0 = 0). + fold not. + + .. coqtop:: none + + Abort. + + .. tacv:: fold {+ @term} - Equivalent to :n:`fold @term ; ... ; fold @term`. + Equivalent to :n:`fold @term ; ... ; fold @term`. .. tacn:: pattern @term :name: pattern |