diff options
Diffstat (limited to 'src/Util/ForLoop')
| -rw-r--r-- | src/Util/ForLoop/InvariantFramework.v | 2 | ||||
| -rw-r--r-- | src/Util/ForLoop/Unrolling.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/ForLoop/InvariantFramework.v b/src/Util/ForLoop/InvariantFramework.v index 503cfcdc3..2bff6bef9 100644 --- a/src/Util/ForLoop/InvariantFramework.v +++ b/src/Util/ForLoop/InvariantFramework.v @@ -16,7 +16,7 @@ Lemma repeat_function_ind {stateT} (P : nat -> stateT -> Prop) : P 0 (repeat_function body count st). Proof. revert dependent st; revert dependent body; revert dependent P. - induction count; intros; [ exact Pbefore | ]. + induction count as [|? IHcount]; intros P body Pbody st Pbefore; [ exact Pbefore | ]. { rewrite repeat_function_unroll1_end; apply Pbody; [ omega | ]. apply (IHcount (fun c => P (S c))); auto with omega. } Qed. 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. |