diff options
Diffstat (limited to 'src/Util/ForLoop/Unrolling.v')
| -rw-r--r-- | src/Util/ForLoop/Unrolling.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ForLoop/Unrolling.v b/src/Util/ForLoop/Unrolling.v index e0518f39a..95b46e711 100644 --- a/src/Util/ForLoop/Unrolling.v +++ b/src/Util/ForLoop/Unrolling.v @@ -31,7 +31,7 @@ Section with_body. : repeat_function body (S count) st = body 1 (repeat_function (fun count => body (S count)) count st). Proof using Type. - revert st; induction count; [ reflexivity | ]. + revert st; induction count as [|? IHcount]; [ reflexivity | ]. intros; simpl in *; rewrite <- IHcount; reflexivity. Qed. |