Skip to content

Commit

Permalink
Fix coqdoc comment in Tutorial_Chaining_Tactics.v
Browse files Browse the repository at this point in the history
  • Loading branch information
thomas-lamiaux authored Nov 4, 2024
1 parent 0d3ab6e commit 7a1004a
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions src/Tutorial_Chaining_Tactics.v
Original file line number Diff line number Diff line change
Expand Up @@ -502,8 +502,7 @@ Section Chaining.
- Fail assumption.
Abort.

(***
- 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
Consider proving the same goal as before but with [A] instantiated to [nat].
You would expect that in both cases, [repeat constructor] gets you into proving
Expand Down

0 comments on commit 7a1004a

Please sign in to comment.