We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 0d3ab6e commit 7a1004aCopy full SHA for 7a1004a
src/Tutorial_Chaining_Tactics.v
@@ -502,8 +502,7 @@ Section Chaining.
502
- Fail assumption.
503
Abort.
504
505
-(***
506
- - 2. [repeat] will apply a tactic as much as possible, it can be more than what you expect
+(** - 2. [repeat] will apply a tactic as much as possible, it can be more than what you expect
507
508
Consider proving the same goal as before but with [A] instantiated to [nat].
509
You would expect that in both cases, [repeat constructor] gets you into proving
0 commit comments